diff options
| author | coqbot-app[bot] | 2020-09-29 09:02:05 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-29 09:02:05 +0000 |
| commit | ff74bba7c4ef0c6f3e17944b015e05fc23bad1af (patch) | |
| tree | 4d7ccf4a2eaf50ba4156f5a8040188c649efe893 | |
| parent | 982c28216f3eb49abfd6b97c69b8fc116c813117 (diff) | |
| parent | cc4494897f0897f5795c2bd25fc06d4b07c73667 (diff) | |
Merge PR #13039: Lint stdlib with -mangle-names #3
Reviewed-by: anton-trunov
31 files changed, 569 insertions, 566 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 1db3f87cac..74d1e391c4 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -110,7 +110,7 @@ Section Between. Lemma between_in_int : forall k l, between k l -> forall r, in_int k l r -> P r. Proof. - induction 1; intros. + intro k; induction 1 as [|l]; intros r ?. - absurd (k < k). { auto with arith. } eapply in_int_lt; eassumption. - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith. @@ -125,7 +125,7 @@ Section Between. Lemma exists_in_int : forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. Proof. - induction 1 as [* ? (p, ?, ?)|]. + induction 1 as [* ? (p, ?, ?)|l]. - exists p; auto with arith. - exists l; auto with arith. Qed. @@ -154,7 +154,7 @@ Section Between. between k l -> (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. Proof. - induction 1; red; intros. + intro k; induction 1 as [|l]; red; intros. - absurd (k < k); auto with arith. - absurd (Q l). { auto with arith. } destruct (exists_in_int k (S l)) as (l',[],?). diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 341dd7de5d..1afc49b7ff 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -21,7 +21,7 @@ Defined. Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. Proof. - induction n in m |- *; destruct m; auto with arith. + induction n as [|n IHn] in m |- *; destruct m as [|m]; auto with arith. destruct (IHn m) as [H|H]; auto with arith. destruct H; auto with arith. Defined. @@ -33,9 +33,9 @@ Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. - induction n in m |- *. + induction n as [|n IHn] in m |- *. - left; auto with arith. - - destruct m. + - destruct m as [|m]. + right; auto with arith. + elim (IHn m); [left|right]; auto with arith. Defined. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 62a0f0a0ae..593d8c5934 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -34,7 +34,7 @@ Hint Resolve eq_nat_refl: arith. Theorem eq_nat_is_eq n m : eq_nat n m <-> n = m. Proof. split. - - revert m; induction n; destruct m; simpl; contradiction || auto. + - revert m; induction n; intro m; destruct m; simpl; contradiction || auto. - intros <-; apply eq_nat_refl. Qed. @@ -53,12 +53,12 @@ Hint Immediate eq_eq_nat eq_nat_eq: arith. Theorem eq_nat_elim : forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. Proof. - intros; replace m with n; auto with arith. + intros n P ? m ?; replace m with n; auto with arith. Qed. Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. Proof. - induction n; destruct m; simpl. + intro n; induction n as [|n IHn]; intro m; destruct m; simpl. - left; trivial. - right; intro; trivial. - right; intro; trivial. @@ -96,7 +96,7 @@ Qed. Definition beq_nat_eq : forall n m, true = (n =? m) -> n = m. Proof. - induction n; destruct m; simpl. + intro n; induction n as [|n IHn]; intro m; destruct m; simpl. - reflexivity. - discriminate. - discriminate. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 0871c4af67..f87d7e810a 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -33,7 +33,7 @@ Qed. Lemma fact_le n m : n <= m -> fact n <= fact m. Proof. - induction 1. + induction 1 as [|m ?]. - apply le_n. - simpl. transitivity (fact m). trivial. apply Nat.le_add_r. Qed. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 4f17a7a8d3..4e71465452 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -80,7 +80,7 @@ Lemma le_elim_rel : (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> forall n m, n <= m -> P n m. Proof. - intros P H0 HS. + intros P H0 HS n. induction n; trivial. intros m Le. elim Le; auto with arith. Qed. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 507d956e81..d7f703e6e4 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -158,7 +158,7 @@ Fixpoint mult_acc (s:nat) m n : nat := Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. - induction n as [| n IHn]; simpl; auto. + intro n; induction n as [| n IHn]; simpl; auto. intros. rewrite Nat.add_assoc, IHn. f_equal. rewrite Nat.add_comm. apply plus_tail_plus. Qed. diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index 6f5339227a..37704704a0 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -75,7 +75,9 @@ Theorem recursion_succ : Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). Proof. -unfold Proper, respectful in *; induction n; simpl; auto. +unfold Proper, respectful in *. +intros A Aeq a f ? ? n. +induction n; simpl; auto. Qed. (** ** Remaining constants not defined in Coq.Init.Nat *) @@ -126,7 +128,7 @@ Qed. Lemma sub_succ_r n m : n - (S m) = pred (n - m). Proof. -revert m. induction n; destruct m; simpl; auto. apply sub_0_r. +revert m. induction n; intro m; destruct m; simpl; auto. apply sub_0_r. Qed. Lemma mul_0_l n : 0 * n = 0. @@ -136,9 +138,9 @@ Qed. Lemma mul_succ_l n m : S n * m = n * m + m. Proof. -assert (succ_r : forall x y, x+S y = S(x+y)) by now induction x. +assert (succ_r : forall x y, x+S y = S(x+y)) by now intro x; induction x. assert (comm : forall x y, x+y = y+x). -{ induction x; simpl; auto. intros; rewrite succ_r; now f_equal. } +{ intro x; induction x; simpl; auto. intros; rewrite succ_r; now f_equal. } now rewrite comm. Qed. @@ -152,7 +154,7 @@ Qed. Lemma eqb_eq n m : eqb n m = true <-> n = m. Proof. revert m. - induction n; destruct m; simpl; rewrite ?IHn; split; try easy. + induction n as [|n IHn]; intro m; destruct m; simpl; rewrite ?IHn; split; try easy. - now intros ->. - now injection 1. Qed. @@ -160,7 +162,7 @@ Qed. Lemma leb_le n m : (n <=? m) = true <-> n <= m. Proof. revert m. - induction n; destruct m; simpl. + induction n as [|n IHn]; intro m; destruct m; simpl. - now split. - split; trivial. intros; apply Peano.le_0_n. - now split. @@ -178,7 +180,7 @@ Qed. Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}. Proof. - induction n; destruct m. + intro n; induction n as [|n IHn]; intro m; destruct m as [|m]. - now left. - now right. - now right. @@ -193,12 +195,14 @@ Defined. Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m. Proof. - revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy. + revert m; induction n as [|n IHn]; intro m; destruct m; + simpl; rewrite ?IHn; split; auto; easy. Qed. Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m. Proof. - revert m; induction n; destruct m; simpl; rewrite ?IHn; split; try easy. + revert m; induction n as [|n IHn]; intro m; destruct m; + simpl; rewrite ?IHn; split; try easy. - intros _. apply Peano.le_n_S, Peano.le_0_n. - apply Peano.le_n_S. - apply Peano.le_S_n. @@ -206,7 +210,7 @@ Qed. Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m. Proof. - revert m; induction n; destruct m; simpl; rewrite ?IHn. + revert m; induction n as [|n IHn]; intro m; destruct m; simpl; rewrite ?IHn. - now split. - split; intros. apply Peano.le_0_n. easy. - split. now destruct 1. inversion 1. @@ -215,7 +219,7 @@ Qed. Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m). Proof. - revert m; induction n; destruct m; simpl; trivial. + revert m; induction n; intro m; destruct m; simpl; trivial. Qed. Lemma compare_succ n m : (S n ?= S m) = (n ?= m). @@ -292,7 +296,7 @@ Lemma Even_2 n : Even n <-> Even (S (S n)). Proof. split; intros (m,H). - exists (S m). rewrite H. simpl. now rewrite plus_n_Sm. - - destruct m; try discriminate. + - destruct m as [|m]; try discriminate. exists m. simpl in H. rewrite <- plus_n_Sm in H. now inversion H. Qed. @@ -305,7 +309,7 @@ Lemma Odd_2 n : Odd n <-> Odd (S (S n)). Proof. split; intros (m,H). - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m). - - destruct m; try discriminate. + - destruct m as [|m]; try discriminate. exists m. simpl in H. rewrite <- plus_n_Sm in H. inversion H. simpl. now rewrite <- !plus_n_Sm, <- !plus_n_O. Qed. @@ -316,7 +320,7 @@ Import Private_Parity. Lemma even_spec : forall n, even n = true <-> Even n. Proof. fix even_spec 1. - destruct n as [|[|n]]; simpl. + intro n; destruct n as [|[|n]]; simpl. - split; [ now exists 0 | trivial ]. - split; [ discriminate | intro H; elim (Even_1 H) ]. - rewrite even_spec. apply Even_2. @@ -326,7 +330,7 @@ Lemma odd_spec : forall n, odd n = true <-> Odd n. Proof. unfold odd. fix odd_spec 1. - destruct n as [|[|n]]; simpl. + intro n; destruct n as [|[|n]]; simpl. - split; [ discriminate | intro H; elim (Odd_0 H) ]. - split; [ now exists 0 | trivial ]. - rewrite odd_spec. apply Odd_2. @@ -338,9 +342,9 @@ Lemma divmod_spec : forall x y q u, u <= y -> let (q',u') := divmod x y q u in x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y. Proof. - induction x. + intro x; induction x as [|x IHx]. - simpl; intuition. - - intros y q u H. destruct u; simpl divmod. + - intros y q u H. destruct u as [|u]; simpl divmod. + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). intros (EQ,LE); split; trivial. rewrite <- EQ, sub_0_r, sub_diag, add_0_r. @@ -356,7 +360,7 @@ Qed. Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y. Proof. intros Hy. - destruct y; [ now elim Hy | clear Hy ]. + destruct y as [|y]; [ now elim Hy | clear Hy ]. unfold div, modulo. generalize (divmod_spec x y 0 y (le_n y)). destruct divmod as (q,u). @@ -380,7 +384,7 @@ Lemma sqrt_iter_spec : forall k p q r, let s := sqrt_iter k p q r in s*s <= k + p*p + (q - r) < (S s)*(S s). Proof. - induction k. + intro k; induction k as [|k IHk]. - (* k = 0 *) simpl; intros p q r Hq Hr. split. @@ -391,7 +395,7 @@ Proof. apply add_le_mono_l. rewrite <- Hq. apply le_sub_l. - (* k = S k' *) - destruct r. + intros p q r; destruct r as [|r]. + (* r = 0 *) intros Hq _. replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))). @@ -427,7 +431,7 @@ Lemma log2_iter_spec : forall k p q r, let s := log2_iter k p q r in 2^s <= k + q < 2^(S s). Proof. - induction k. + intro k; induction k as [|k IHk]. - (* k = 0 *) intros p q r EQ LT. simpl log2_iter. cbv zeta. split. @@ -438,7 +442,7 @@ Proof. + rewrite EQ, add_comm. apply add_lt_mono_l. apply lt_succ_r, le_0_l. - (* k = S k' *) - intros p q r EQ LT. destruct r. + intros p q r EQ LT. destruct r as [|r]. + (* r = 0 *) rewrite add_succ_r, add_0_r in EQ. rewrite add_succ_l, <- add_succ_r. apply IHk. @@ -537,7 +541,7 @@ Lemma le_div2 n : div2 (S n) <= n. Proof. revert n. fix le_div2 1. - destruct n; simpl; trivial. apply lt_succ_r. + intro n; destruct n as [|n]; simpl; trivial. apply lt_succ_r. destruct n; [simpl|]; trivial. now constructor. Qed. @@ -550,7 +554,7 @@ Qed. Lemma div2_decr a n : a <= S n -> div2 a <= n. Proof. - destruct a; intros H. + destruct a as [|a]; intros H. - simpl. apply le_0_l. - apply succ_le_mono in H. apply le_trans with a; [ apply le_div2 | trivial ]. @@ -563,7 +567,7 @@ Qed. Lemma testbit_0_l : forall n, testbit 0 n = false. Proof. - now induction n. + now intro n; induction n. Qed. Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. @@ -592,7 +596,7 @@ Qed. Lemma shiftr_specif : forall a n m, testbit (shiftr a n) m = testbit a (m+n). Proof. - induction n; intros m. trivial. + intros a n; induction n as [|n IHn]; intros m. trivial. now rewrite add_0_r. now rewrite add_succ_r, <- add_succ_l, <- IHn. Qed. @@ -600,7 +604,7 @@ Qed. Lemma shiftl_specif_high : forall a n m, n<=m -> testbit (shiftl a n) m = testbit a (m-n). Proof. - induction n; intros m H. trivial. + intros a n; induction n as [|n IHn]; intros m H. trivial. now rewrite sub_0_r. destruct m. inversion H. simpl. apply succ_le_mono in H. @@ -611,7 +615,7 @@ Qed. Lemma shiftl_spec_low : forall a n m, m<n -> testbit (shiftl a n) m = false. Proof. - induction n; intros m H. inversion H. + intros a n; induction n as [|n IHn]; intros m H. inversion H. change (shiftl a (S n)) with (double (shiftl a n)). destruct m; simpl. unfold odd. apply negb_false_iff. @@ -623,7 +627,7 @@ Qed. Lemma div2_bitwise : forall op n a b, div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b). Proof. - intros. unfold bitwise; fold bitwise. + intros op n a b. unfold bitwise; fold bitwise. destruct (op (odd a) (odd b)). now rewrite div2_succ_double. now rewrite add_0_l, div2_double. @@ -632,7 +636,7 @@ Qed. Lemma odd_bitwise : forall op n a b, odd (bitwise op (S n) a b) = op (odd a) (odd b). Proof. - intros. unfold bitwise; fold bitwise. + intros op n a b. unfold bitwise; fold bitwise. destruct (op (odd a) (odd b)). apply odd_spec. rewrite add_comm. eexists; eauto. unfold odd. apply negb_false_iff. apply even_spec. @@ -644,7 +648,7 @@ Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) -> testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). Proof. intros op Hop. - induction n; intros m a b Ha. + intro n; induction n as [|n IHn]; intros m a b Ha. simpl. inversion Ha; subst. now rewrite testbit_0_l. destruct m. apply odd_bitwise. @@ -657,7 +661,7 @@ Lemma testbit_bitwise_2 : forall op, op false false = false -> testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). Proof. intros op Hop. - induction n; intros m a b Ha Hb. + intro n; induction n as [|n IHn]; intros m a b Ha Hb. simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l. destruct m. apply odd_bitwise. @@ -682,11 +686,11 @@ Lemma lor_spec a b n : Proof. unfold lor. apply testbit_bitwise_2. - trivial. - - destruct (compare_spec a b). + - destruct (compare_spec a b) as [H|H|H]. + rewrite max_l; subst; trivial. + apply lt_le_incl in H. now rewrite max_r. + apply lt_le_incl in H. now rewrite max_l. - - destruct (compare_spec a b). + - destruct (compare_spec a b) as [H|H|H]. + rewrite max_r; subst; trivial. + apply lt_le_incl in H. now rewrite max_r. + apply lt_le_incl in H. now rewrite max_l. @@ -697,11 +701,11 @@ Lemma lxor_spec a b n : Proof. unfold lxor. apply testbit_bitwise_2. - trivial. - - destruct (compare_spec a b). + - destruct (compare_spec a b) as [H|H|H]. + rewrite max_l; subst; trivial. + apply lt_le_incl in H. now rewrite max_r. + apply lt_le_incl in H. now rewrite max_l. - - destruct (compare_spec a b). + - destruct (compare_spec a b) as [H|H|H]. + rewrite max_r; subst; trivial. + apply lt_le_incl in H. now rewrite max_r. + apply lt_le_incl in H. now rewrite max_l. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index a673a1119f..9a7a397023 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -16,7 +16,7 @@ Implicit Types m n x y : nat. Theorem O_or_S n : {m : nat | S m = n} + {0 = n}. Proof. - induction n. + induction n as [|n IHn]. - now right. - left; exists n; auto. Defined. @@ -47,7 +47,7 @@ pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2). 2: reflexivity. generalize def_n2; revert le_mn1 le_mn2. generalize n0 at 1 4 5 7; intros n1 le_mn1. -destruct le_mn1; intros le_mn2; destruct le_mn2. +destruct le_mn1 as [|? le_mn1]; intros le_mn2; destruct le_mn2 as [|? le_mn2]. + now intros def_n0; rewrite (UIP_nat _ _ def_n0 eq_refl). + intros def_n0; generalize le_mn2; rewrite <-def_n0; intros le_mn0. now destruct (Nat.nle_succ_diag_l _ le_mn0). diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index ec7426e648..5da7738adc 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -156,7 +156,7 @@ Fixpoint tail_plus n m : nat := Lemma plus_tail_plus : forall n m, n + m = tail_plus n m. Proof. -induction n as [| n IHn]; simpl; auto. +intro n; induction n as [| n IHn]; simpl; auto. intro m; rewrite <- IHn; simpl; auto. Qed. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 3bfef93726..ebd909c1dc 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -27,8 +27,8 @@ Definition gtof (a b:A) := f b > f a. Theorem well_founded_ltof : well_founded ltof. Proof. assert (H : forall n (a:A), f a < n -> Acc ltof a). - { induction n. - - intros; absurd (f a < 0); auto with arith. + { intro n; induction n as [|n IHn]. + - intros a Ha; absurd (f a < 0); auto with arith. - intros a Ha. apply Acc_intro. unfold ltof at 1. intros b Hb. apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } intros a. apply (H (S (f a))). auto with arith. @@ -69,8 +69,8 @@ Theorem induction_ltof1 : Proof. intros P F. assert (H : forall n (a:A), f a < n -> P a). - { induction n. - - intros; absurd (f a < 0); auto with arith. + { intro n; induction n as [|n IHn]. + - intros a Ha; absurd (f a < 0); auto with arith. - intros a Ha. apply F. unfold ltof. intros b Hb. apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } intros a. apply (H (S (f a))). auto with arith. @@ -107,8 +107,8 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y. Theorem well_founded_lt_compat : well_founded R. Proof. assert (H : forall n (a:A), f a < n -> Acc R a). - { induction n. - - intros; absurd (f a < 0); auto with arith. + { intro n; induction n as [|n IHn]. + - intros a Ha; absurd (f a < 0); auto with arith. - intros a Ha. apply Acc_intro. intros b Hb. apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } intros a. apply (H (S (f a))). auto with arith. @@ -212,26 +212,26 @@ Section LT_WF_REL. Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x. Proof. intros x [n fxn]; generalize dependent x. - pattern n; apply lt_wf_ind; intros. - constructor; intros. + pattern n; apply lt_wf_ind; intros n0 H x fxn. + constructor; intros y H0. destruct (F_compat y x) as (x0,H1,H2); trivial. apply (H x0); auto. Qed. Theorem well_founded_inv_lt_rel_compat : well_founded R. Proof. - constructor; intros. - case (F_compat y a); trivial; intros. + intro a; constructor; intros y H. + case (F_compat y a); trivial; intros x **. apply acc_lt_rel; trivial. exists x; trivial. Qed. End LT_WF_REL. -Lemma well_founded_inv_rel_inv_lt_rel : - forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). +Lemma well_founded_inv_rel_inv_lt_rel (A:Set) (F:A -> nat -> Prop) : + well_founded (inv_lt_rel A F). Proof. - intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. + apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. Qed. (** A constructive proof that any non empty decidable subset of @@ -253,8 +253,8 @@ Proof. intros P Pdec (n0,HPn0). assert (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') - \/ (forall n', P n' -> n<=n')). - { induction n. + \/ (forall n', P n' -> n<=n')) as H. + { intro n; induction n as [|n IHn]. - right. intros. apply Nat.le_0_l. - destruct IHn as [(n' & IH1 & IH2)|IH]. + left. exists n'; auto with arith. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 76633ab201..4cc3597029 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -74,31 +74,31 @@ Section Facts. (** *** Generic facts *) (** Discrimination *) - Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l. + Theorem nil_cons (x:A) (l:list A) : [] <> x :: l. Proof. - intros; discriminate. + discriminate. Qed. (** Destruction *) - Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = []}. + Theorem destruct_list (l : list A) : {x:A & {tl:list A | l = x::tl}}+{l = []}. Proof. induction l as [|a tail]. right; reflexivity. left; exists a, tail; reflexivity. Qed. - Lemma hd_error_tl_repr : forall l (a:A) r, + Lemma hd_error_tl_repr 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. + - unfold hd_error, tl; split; firstorder discriminate. - 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. + Lemma hd_error_some_nil 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): @@ -114,9 +114,9 @@ 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 (l : list A) (x : A) : hd_error (x::l) = Some x. Proof. - intros; simpl; reflexivity. + simpl; reflexivity. Qed. @@ -125,41 +125,41 @@ Section Facts. (**************************) (** Discrimination *) - Theorem app_cons_not_nil : forall (x y:list A) (a:A), [] <> x ++ a :: y. + Theorem app_cons_not_nil (x y:list A) (a:A) : [] <> x ++ a :: y. Proof. unfold not. - destruct x as [| a l]; simpl; intros. + destruct x; simpl; intros H. discriminate H. discriminate H. Qed. (** Concat with [nil] *) - Theorem app_nil_l : forall l:list A, [] ++ l = l. + Theorem app_nil_l (l:list A) : [] ++ l = l. Proof. reflexivity. Qed. - Theorem app_nil_r : forall l:list A, l ++ [] = l. + Theorem app_nil_r (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 (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 (l m n:list A) : l ++ m ++ n = (l ++ m) ++ n. Proof. - intros l m n; induction l; simpl; f_equal; auto. + 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 (l m n:list A) : (l ++ m) ++ n = l ++ m ++ n. Proof. auto using app_assoc. Qed. @@ -167,42 +167,41 @@ 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 (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 (l l':list A) : l ++ l' = [] -> l = [] /\ l' = []. Proof. destruct l as [| x l]; destruct l' as [| y l']; simpl; auto. intro; discriminate. intros H; discriminate H. Qed. - Theorem app_eq_unit : - forall (x y:list A) (a:A), + Theorem app_eq_unit (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] ]; + destruct x as [|a' l]; [ destruct y as [|a' l] | destruct y as [| a0 l0] ]; simpl. - intros a H; discriminate H. + intros H; discriminate H. left; split; auto. - right; split; auto. + intro H; right; split; auto. generalize H. generalize (app_nil_r l); intros E. rewrite -> E; auto. - intros. + intros H. injection H as [= H H0]. - assert ([] = l ++ a0 :: l0) by auto. + assert ([] = l ++ a0 :: l0) as H1 by auto. apply app_cons_not_nil in H1 as []. Qed. - Lemma elt_eq_unit : forall l1 l2 (a b : A), + Lemma elt_eq_unit l1 l2 (a b : A) : l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = []. Proof. - intros l1 l2 a b Heq. + intros Heq. apply app_eq_unit in Heq. now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2. Qed. @@ -210,7 +209,7 @@ Section Facts. Lemma app_inj_tail_iff : forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] <-> x = y /\ a = b. Proof. - induction x as [| x l IHl]; + intro x; induction x as [| x l IHl]; intro y; [ destruct y as [| a l] | destruct y as [| a l0] ]; simpl; auto. - intros a b. split. @@ -220,7 +219,7 @@ Section Facts. + intros [= H1 H0]. apply app_cons_not_nil in H0 as []. + intros [H0 H1]. inversion H0. - intros a b. split. - + intros [= H1 H0]. assert ([] = l ++ [a]) by auto. apply app_cons_not_nil in H as []. + + intros [= H1 H0]. assert ([] = l ++ [a]) as H by auto. apply app_cons_not_nil in H as []. + intros [H0 H1]. inversion H0. - intros a0 b. split. + intros [= <- H0]. specialize (IHl l0 a0 b). apply IHl in H0. destruct H0. subst. split; auto. @@ -237,7 +236,7 @@ Section Facts. Lemma app_length : forall l l' : list A, length (l++l') = length l + length l'. Proof. - induction l; simpl; auto. + intro l; induction l; simpl; auto. Qed. Lemma last_length : forall (l : list A) a, length (l ++ a :: nil) = S (length l). @@ -249,7 +248,7 @@ Section Facts. Lemma app_inv_head_iff: forall l l1 l2 : list A, l ++ l1 = l ++ l2 <-> l1 = l2. Proof. - induction l; split; intros; simpl; auto. + intro l; induction l as [|? l IHl]; split; intros H; simpl; auto. - apply IHl. inversion H. auto. - subst. auto. Qed. @@ -264,7 +263,7 @@ Section Facts. 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]; + intro l1; induction l1 as [ | x1 l1]; intro l2; destruct l2 as [ | x2 l2]; simpl; auto; intros l H. absurd (length (x2 :: l2 ++ l) <= length l). simpl; rewrite app_length; auto with arith. @@ -344,7 +343,7 @@ Section Facts. Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. Proof. - induction l; simpl; destruct 1. + intros x l; induction l as [|a l IHl]; simpl; [destruct 1|destruct 1 as [?|H]]. subst a; auto. exists [], l; auto. destruct (IHl H) as (l1,(l2,H0)). @@ -375,7 +374,7 @@ Section Facts. (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]. + intros H a l; induction l as [| a0 l IHl]. right; apply in_nil. destruct (H a0 a); simpl; auto. destruct IHl; simpl; auto. @@ -425,8 +424,8 @@ Section Elts. Lemma nth_in_or_default : 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 l d; revert n; induction l as [|? ? IHl]. + - intro n; right; destruct n; trivial. - intros [|n]; simpl. * left; auto. * destruct (IHl n); auto. @@ -455,7 +454,7 @@ Section Elts. 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; intro n; induction n; intros [ | ] ?; simpl; auto. Qed. (** Results about [nth] *) @@ -463,7 +462,7 @@ Section Elts. Lemma nth_In : 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. + unfold lt; intro n; induction n as [| n hn]; simpl; intro l. - destruct l; simpl; [ inversion 2 | auto ]. - destruct l; simpl. * inversion 2. @@ -483,7 +482,8 @@ Section Elts. Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d. Proof. - induction l; destruct n; simpl; intros; auto. + intro l; induction l as [|? ? IHl]; intro n; destruct n; + simpl; intros d H; auto. - inversion H. - apply IHl; auto with arith. Qed. @@ -491,7 +491,7 @@ Section Elts. Lemma nth_indep : forall l n d d', n < length l -> nth n l d = nth n l d'. Proof. - induction l. + intro l; induction l. - inversion 1. - intros [|n] d d'; simpl; auto with arith. Qed. @@ -499,7 +499,7 @@ Section Elts. Lemma app_nth1 : forall l l' d n, n < length l -> nth n (l++l') d = nth n l d. Proof. - induction l. + intro l; induction l. - inversion 1. - intros l' d [|n]; simpl; auto with arith. Qed. @@ -507,7 +507,7 @@ Section Elts. Lemma app_nth2 : 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. + intro l; induction l as [|? ? IHl]; intros l' d [|n]; auto. - inversion 1. - intros; simpl; rewrite IHl; auto with arith. Qed. @@ -541,7 +541,8 @@ Section Elts. Lemma nth_ext : forall l l' d d', length l = length l' -> (forall n, n < length l -> nth n l d = nth n l' d') -> l = l'. Proof. - induction l; intros l' d d' Hlen Hnth; destruct l' as [| b l']. + intro l; induction l as [|a l IHl]; + intros l' d d' Hlen Hnth; destruct l' as [| b l']. - reflexivity. - inversion Hlen. - inversion Hlen. @@ -575,7 +576,7 @@ Section Elts. Lemma nth_error_None l n : nth_error l n = None <-> length l <= n. Proof. - revert n. induction l; destruct n; simpl. + revert n. induction l as [|? ? IHl]; intro n; destruct n; simpl. - split; auto. - split; auto with arith. - split; now auto with arith. @@ -584,7 +585,7 @@ Section Elts. Lemma nth_error_Some l n : nth_error l n <> None <-> n < length l. Proof. - revert n. induction l; destruct n; simpl. + revert n. induction l as [|? ? IHl]; intro n; destruct n; simpl. - split; [now destruct 1 | inversion 1]. - split; [now destruct 1 | inversion 1]. - split; now auto with arith. @@ -605,7 +606,7 @@ Section Elts. 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 as [|n IHn]; intros [|a l] H; auto; try solve [inversion H]. simpl in *. apply IHn. auto with arith. Qed. @@ -613,7 +614,7 @@ Section Elts. 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 as [|n IHn]; intros [|a l] H; auto; try solve [inversion H]. simpl in *. apply IHn. auto with arith. Qed. @@ -632,7 +633,7 @@ Section Elts. n < length l -> nth_error l n = Some (nth n l d). Proof. intros l n d H. - apply nth_split with (d:=d) in H. destruct H as [l1 [l2 [H H']]]. + apply (nth_split _ d) in H. destruct H as [l1 [l2 [H H']]]. subst. rewrite H. rewrite nth_error_app2; [|auto]. rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity. Qed. @@ -653,7 +654,7 @@ Section Elts. Lemma last_last : forall l a d, last (l ++ [a]) d = a. Proof. - induction l; intros; [ reflexivity | ]. + intro l; induction l as [|? l IHl]; intros; [ reflexivity | ]. simpl; rewrite IHl. destruct l; reflexivity. Qed. @@ -670,17 +671,17 @@ Section Elts. Lemma app_removelast_last : forall l d, l <> [] -> l = removelast l ++ [last l d]. Proof. - induction l. + intro l; induction l as [|? l IHl]. destruct 1; auto. intros d _. - destruct l; auto. + destruct l as [|a0 l]; auto. 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]}}. Proof. - induction l. + intro l; induction l as [|a l IHl]. destruct 1; auto. intros _. destruct l. @@ -693,10 +694,10 @@ Section Elts. Lemma removelast_app : forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'. Proof. - induction l. + intro l; induction l as [|? l IHl]. simpl; auto. - simpl; intros. - assert (l++l' <> []). + simpl; intros l' H. + assert (l++l' <> []) as H0. destruct l. simpl; auto. simpl; discriminate. @@ -733,7 +734,7 @@ Section Elts. Lemma remove_app : forall x l1 l2, remove x (l1 ++ l2) = remove x l1 ++ remove x l2. Proof. - induction l1; intros l2; simpl. + intros x l1; induction l1 as [|a l1 IHl1]; intros l2; simpl. - reflexivity. - destruct (eq_dec x a). + apply IHl1. @@ -743,7 +744,7 @@ Section Elts. Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). Proof. - induction l as [|x l]; auto. + intro l; induction l as [|x l IHl]; auto. intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. apply IHl. unfold not; intro HF; simpl in HF; destruct HF; auto. @@ -760,7 +761,7 @@ Section Elts. Lemma in_remove: forall l x y, In x (remove y l) -> In x l /\ x <> y. Proof. - induction l as [|z l]; intros x y Hin. + intro l; induction l as [|z l IHl]; intros x y Hin. - inversion Hin. - simpl in Hin. destruct (eq_dec y z) as [Heq|Hneq]; subst; split. @@ -775,7 +776,7 @@ Section Elts. Lemma in_in_remove : forall l x y, x <> y -> In x l -> In x (remove y l). Proof. - induction l as [|z l]; simpl; intros x y Hneq Hin. + intro l; induction l as [|z l IHl]; simpl; intros x y Hneq Hin. - apply Hin. - destruct (eq_dec y z); subst. + destruct Hin. @@ -788,7 +789,7 @@ Section Elts. Lemma remove_remove_comm : forall l x y, remove x (remove y l) = remove y (remove x l). Proof. - induction l as [| z l]; simpl; intros x y. + intro l; induction l as [| z l IHl]; simpl; intros x y. - reflexivity. - destruct (eq_dec y z); simpl; destruct (eq_dec x z); try rewrite IHl; auto. + subst; symmetry; apply remove_cons. @@ -800,7 +801,7 @@ Section Elts. Lemma remove_length_le : forall l x, length (remove x l) <= length l. Proof. - induction l as [|y l IHl]; simpl; intros x; trivial. + intro l; induction l as [|y l IHl]; simpl; intros x; trivial. destruct (eq_dec x y); simpl. - rewrite IHl; constructor; reflexivity. - apply (proj1 (Nat.succ_le_mono _ _) (IHl x)). @@ -808,7 +809,7 @@ Section Elts. Lemma remove_length_lt : forall l x, In x l -> length (remove x l) < length l. Proof. - induction l as [|y l IHl]; simpl; intros x Hin. + intro l; induction l as [|y l IHl]; simpl; intros x Hin. - contradiction Hin. - destruct Hin as [-> | Hin]. + destruct (eq_dec x x); intuition. @@ -833,7 +834,7 @@ Section Elts. (** 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. + induction l as [|y l IHl]; simpl. - split; [destruct 1 | apply gt_irrefl]. - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition. Qed. @@ -892,8 +893,8 @@ Section ListOps. 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]. + intro x; induction x as [| a l IHl]. + intro y; destruct y as [| a l]. simpl. auto. @@ -908,13 +909,13 @@ Section ListOps. Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l. Proof. - intros. + intros l a. apply (rev_app_distr l [a]); simpl; auto. Qed. Lemma rev_involutive : forall l:list A, rev (rev l) = l. Proof. - induction l as [| a l IHl]. + intro l; induction l as [| a l IHl]. simpl; auto. simpl. @@ -933,11 +934,11 @@ Section ListOps. Lemma in_rev : forall l x, In x l <-> In x (rev l). Proof. - induction l. + intro l; induction l. simpl; intuition. intros. simpl. - intuition. + split; intro H; [destruct H|]. subst. apply in_or_app; right; simpl; auto. apply in_or_app; left; firstorder. @@ -946,7 +947,7 @@ Section ListOps. Lemma rev_length : forall l, length (rev l) = length l. Proof. - induction l;simpl; auto. + intro l; induction l as [|? l IHl];simpl; auto. rewrite app_length. rewrite IHl. simpl. @@ -956,9 +957,9 @@ Section ListOps. 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. + intro l; induction l as [|a l IHl]. + intros d n H; inversion H. + intros ? n H. simpl in H. simpl (rev (a :: l)). simpl (length (a :: l) - S n). @@ -988,7 +989,7 @@ Section ListOps. Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'. Proof. - induction l; simpl; auto; intros. + intro l; induction l; simpl; auto; intros. rewrite <- app_assoc; firstorder. Qed. @@ -1010,20 +1011,20 @@ Section ListOps. (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> forall l:list A, P (rev l). Proof. - induction l; auto. + intros P ? ? l; 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. Proof. - intros. + intros P H H0 l. generalize (rev_involutive l). intros E; rewrite <- E. apply (rev_list_ind P). - auto. - simpl. - intros. + intros a l0 ?. apply (H0 a (rev l0)). auto. Qed. @@ -1060,10 +1061,10 @@ Section ListOps. Lemma in_concat : forall l y, In y (concat l) <-> exists x, In x l /\ In y x. Proof. - induction l; simpl; split; intros. + intro l; induction l as [|a l IHl]; simpl; intro y; split; intros H. contradiction. destruct H as (x,(H,_)); contradiction. - destruct (in_app_or _ _ _ H). + destruct (in_app_or _ _ _ H) as [H0|H0]. exists a; auto. destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). exists x; auto. @@ -1112,69 +1113,69 @@ Section Map. Lemma in_map : forall (l:list A) (x:A), In x l -> In (f x) (map l). Proof. - induction l; firstorder (subst; auto). + intro l; 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. Proof. - induction l; firstorder (subst; auto). + intro l; induction l; firstorder (subst; auto). Qed. Lemma map_length : forall l, length (map l) = length l. Proof. - induction l; simpl; auto. + intro l; induction l; simpl; auto. Qed. 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. + intro l; induction l; simpl map; intros d n; 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). Proof. - induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto. + intro n; induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto. Qed. Lemma map_app : forall l l', map (l++l') = (map l)++(map l'). Proof. - induction l; simpl; auto. + intro l; induction l as [|a l IHl]; simpl; auto. intros; rewrite IHl; auto. Qed. Lemma map_last : forall l a, map (l ++ [a]) = (map l) ++ [f a]. Proof. - induction l; intros; [ reflexivity | ]. + intro l; induction l as [|a l IHl]; intros; [ reflexivity | ]. simpl; rewrite IHl; reflexivity. Qed. Lemma map_rev : forall l, map (rev l) = rev (map l). Proof. - induction l; simpl; auto. + intro l; induction l as [|a l IHl]; simpl; auto. rewrite map_app. rewrite IHl; auto. Qed. Lemma map_eq_nil : forall l, map l = [] -> l = []. Proof. - destruct l; simpl; reflexivity || discriminate. + intro l; destruct l; simpl; reflexivity || discriminate. Qed. Lemma map_eq_cons : forall l l' b, map l = b :: l' -> exists a tl, l = a :: tl /\ f a = b /\ map tl = l'. Proof. intros l l' b Heq. - destruct l; inversion_clear Heq. + destruct l as [|a l]; inversion_clear Heq. exists a, l; repeat split. Qed. Lemma map_eq_app : forall l l1 l2, map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ map l1' = l1 /\ map l2' = l2. Proof. - induction l; simpl; intros l1 l2 Heq. + intro l; induction l as [|a l IHl]; simpl; intros l1 l2 Heq. - symmetry in Heq; apply app_eq_nil in Heq; destruct Heq; subst. exists nil, nil; repeat split. - destruct l1; simpl in Heq; inversion Heq as [[Heq2 Htl]]. @@ -1215,7 +1216,7 @@ Section Map. flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2. Proof. intros F l1 l2. - induction l1; [ reflexivity | simpl ]. + induction l1 as [|? ? IHl1]; [ reflexivity | simpl ]. rewrite IHl1, app_assoc; reflexivity. Qed. @@ -1223,10 +1224,10 @@ Section Map. In y (flat_map f l) <-> exists x, In x l /\ In y (f x). Proof. clear f Hfinjective. - induction l; simpl; split; intros. + intros f l; induction l as [|a l IHl]; simpl; intros y; split; intros H. contradiction. destruct H as (x,(H,_)); contradiction. - destruct (in_app_or _ _ _ H). + destruct (in_app_or _ _ _ H) as [H0|H0]. exists a; auto. destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). exists x; auto. @@ -1257,33 +1258,33 @@ Qed. Lemma remove_concat A (eq_dec : forall x y : A, {x = y}+{x <> y}) : forall l x, remove eq_dec x (concat l) = flat_map (remove eq_dec x) l. Proof. - intros l x; induction l; [ reflexivity | simpl ]. + intros l x; induction l as [|? ? IHl]; [ reflexivity | simpl ]. rewrite remove_app, IHl; reflexivity. Qed. Lemma map_id : forall (A :Type) (l : list A), map (fun x => x) l = l. Proof. - induction l; simpl; auto; rewrite IHl; auto. + intros A l; induction l as [|? ? IHl]; simpl; auto; rewrite IHl; auto. Qed. 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. + intros A B C f g l; induction l as [|? ? IHl]; simpl; auto. rewrite IHl; auto. 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. Proof. - induction l; simpl; auto. - intros; rewrite H by intuition; rewrite IHl; auto. + intros A B f g l; induction l as [|? ? IHl]; simpl; auto. + intros H; rewrite H by intuition; rewrite IHl; auto. Qed. Lemma ext_in_map : forall (A B : Type)(f g:A->B) l, map f l = map g l -> forall a, In a l -> f a = g a. -Proof. induction l; intros [=] ? []; subst; auto. Qed. +Proof. intros A B f g l; induction l; intros [=] ? []; subst; auto. Qed. Arguments ext_in_map [A B f g l]. @@ -1304,13 +1305,13 @@ Lemma flat_map_ext : forall (A B : Type)(f g : A -> list B), Proof. intros A B f g Hext l. rewrite 2 flat_map_concat_map. - now rewrite map_ext with (g := g). + now rewrite (map_ext _ g). Qed. Lemma nth_nth_nth_map A : forall (l : list A) n d ln dn, n < length ln \/ length l <= dn -> nth (nth n ln dn) l d = nth n (map (fun x => nth x l d) ln) d. Proof. - intros l n d ln dn; revert n; induction ln; intros n Hlen. + intros l n d ln dn; revert n; induction ln as [|? ? IHln]; intros n Hlen. - destruct Hlen as [Hlen|Hlen]. + inversion Hlen. + now rewrite nth_overflow; destruct n. @@ -1336,7 +1337,7 @@ Section Fold_Left_Recursor. 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. + intro l; induction l. simpl; auto. intros. simpl. @@ -1350,7 +1351,7 @@ Lemma fold_left_length : Proof. intros A l. enough (H : forall n, fold_left (fun x _ => S x) l n = n + length l) by exact (H 0). - induction l; simpl; auto. + induction l as [|? ? IHl]; simpl; auto. intros; rewrite IHl. simpl; auto with arith. Qed. @@ -1375,7 +1376,7 @@ 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. Proof. - induction l. + intros A B f l; induction l. simpl; auto. simpl; intros. f_equal; auto. @@ -1384,7 +1385,7 @@ End Fold_Right_Recursor. 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. + intros A B f l; induction l. simpl; auto. intros. simpl. @@ -1398,8 +1399,9 @@ End Fold_Right_Recursor. 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 IHl]; [ simpl; reflexivity | ]. + simpl. rewrite <- IHl. clear IHl. revert a1. + induction l as [|? ? IHl]; [ auto | ]. simpl. intro. rewrite <- assoc. rewrite IHl. rewrite IHl. auto. Qed. @@ -1436,7 +1438,7 @@ End Fold_Right_Recursor. Lemma existsb_exists : forall l, existsb l = true <-> exists x, In x l /\ f x = true. Proof. - induction l as [ | a m IH ]; split; simpl. + intro l; induction l as [ | a m IH ]; split; simpl. - easy. - intros [x [[]]]. - rewrite orb_true_iff; intros [ H | H ]. @@ -1451,9 +1453,9 @@ End Fold_Right_Recursor. Lemma existsb_nth : forall l n d, n < length l -> existsb l = false -> f (nth n l d) = false. Proof. - induction l. + intro l; induction l as [|? ? IHl]. inversion 1. - simpl; intros. + simpl; intros n ? ? H0. destruct (orb_false_elim _ _ H0); clear H0; auto. destruct n ; auto. rewrite IHl; auto with arith. @@ -1462,7 +1464,7 @@ End Fold_Right_Recursor. Lemma existsb_app : forall l1 l2, existsb (l1++l2) = existsb l1 || existsb l2. Proof. - induction l1; intros l2; simpl. + intro l1; induction l1 as [|a ? ?]; intros l2; simpl. solve[auto]. case (f a); simpl; solve[auto]. Qed. @@ -1479,19 +1481,19 @@ End Fold_Right_Recursor. Lemma forallb_forall : forall l, forallb l = true <-> (forall x, In x l -> f x = true). Proof. - induction l; simpl; intuition. - destruct (andb_prop _ _ H1). - congruence. - destruct (andb_prop _ _ H1); auto. - assert (forallb l = true). - apply H0; intuition. - rewrite H1; auto. + intro l; induction l as [|a l IHl]; simpl; [ tauto | split; intro H ]. + + destruct (andb_prop _ _ H); intros a' [?|?]. + - congruence. + - apply IHl; assumption. + + apply andb_true_intro; split. + - apply H; left; reflexivity. + - apply IHl; intros; apply H; right; assumption. Qed. Lemma forallb_app : forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2. Proof. - induction l1; simpl. + intro l1; induction l1 as [|a ? ?]; simpl. solve[auto]. case (f a); simpl; solve[auto]. Qed. @@ -1506,7 +1508,7 @@ End Fold_Right_Recursor. Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true. Proof. - induction l; simpl. + intros x l; induction l as [|a ? ?]; simpl. intuition. intros. case_eq (f a); intros; simpl; intuition congruence. @@ -1522,7 +1524,7 @@ End Fold_Right_Recursor. Lemma concat_filter_map : forall (l : list (list A)), concat (map filter l) = filter (concat l). Proof. - induction l as [| v l IHl]; [auto|]. + intro l; induction l as [| v l IHl]; [auto|]. simpl. rewrite IHl. rewrite filter_app. reflexivity. Qed. @@ -1618,10 +1620,10 @@ End Fold_Right_Recursor. Lemma filter_map : forall (f g : A -> bool) (l : list A), filter f l = filter g l <-> map f l = map g l. Proof. - induction l as [| a l IHl]; [firstorder|]. + intros f g l; induction l as [| a l IHl]; [firstorder|]. simpl. destruct (f a) eqn:Hfa; destruct (g a) eqn:Hga; split; intros H. - - inversion H. apply IHl in H1. rewrite H1. reflexivity. - - inversion H. apply IHl in H1. rewrite H1. reflexivity. + - inversion H as [H1]. apply IHl in H1. rewrite H1. reflexivity. + - inversion H as [H1]. apply IHl in H1. rewrite H1. reflexivity. - assert (Ha : In a (filter g l)). { rewrite <- H. apply in_eq. } apply filter_In in Ha. destruct Ha as [_ Hga']. rewrite Hga in Hga'. inversion Hga'. - inversion H. @@ -1702,9 +1704,9 @@ End Fold_Right_Recursor. 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. - destruct p; destruct a; destruct (split l); simpl in *. - destruct H. + intro l; induction l as [|a l IHl]; simpl; intros p H; auto. + destruct p as [a0 b]; destruct a; destruct (split l); simpl in *. + destruct H as [H|H]. injection H; auto. right; apply (IHl (a0,b) H). Qed. @@ -1712,9 +1714,9 @@ End Fold_Right_Recursor. 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. - destruct p; destruct a; destruct (split l); simpl in *. - destruct H. + intro l; induction l as [|a l IHl]; simpl; intros p H; auto. + destruct p as [a0 b]; destruct a; destruct (split l); simpl in *. + destruct H as [H|H]. injection H; auto. right; apply (IHl (a0,b) H). Qed. @@ -1722,9 +1724,9 @@ End Fold_Right_Recursor. 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. - destruct n; destruct d; simpl; auto. + intro l; induction l as [|a l IHl]. + intros n d; destruct n; destruct d; simpl; auto. + intros n d; destruct n; destruct d; simpl; auto. destruct a; destruct (split l); simpl; auto. destruct a; destruct (split l); simpl in *; auto. apply IHl. @@ -1733,14 +1735,14 @@ End Fold_Right_Recursor. Lemma split_length_l : forall (l:list (A*B)), length (fst (split l)) = length l. Proof. - induction l; simpl; auto. + intro l; induction l as [|a l IHl]; 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. Proof. - induction l; simpl; auto. + intro l; induction l as [|a l IHl]; simpl; auto. destruct a; destruct (split l); simpl; auto. Qed. @@ -1757,7 +1759,7 @@ End Fold_Right_Recursor. Lemma split_combine : forall (l: list (A*B)), let (l1,l2) := split l in combine l1 l2 = l. Proof. - induction l. + intro l; induction l as [|a l IHl]. simpl; auto. destruct a; simpl. destruct (split l); simpl in *. @@ -1767,18 +1769,19 @@ End Fold_Right_Recursor. Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> split (combine l l') = (l,l'). Proof. - induction l, l'; simpl; trivial; try discriminate. + intro l; induction l as [|a l IHl]; intro l'; destruct l'; + simpl; trivial; try discriminate. now intros [= ->%IHl]. 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. Proof. - induction l. + intro l; induction l as [|a l IHl]. simpl; auto. - destruct l'; simpl; auto; intros. + intro l'; destruct l' as [|a0 l']; simpl; auto; intros x y H. contradiction. - destruct H. + destruct H as [H|H]. injection H; auto. right; apply IHl with l' y; auto. Qed. @@ -1786,10 +1789,10 @@ End Fold_Right_Recursor. 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. + intro l; induction l as [|? ? IHl]. simpl; intros; contradiction. - destruct l'; simpl; auto; intros. - destruct H. + intro l'; destruct l'; simpl; auto; intros x y H. + destruct H as [H|H]. injection H; auto. right; apply IHl with x; auto. Qed. @@ -1797,16 +1800,16 @@ End Fold_Right_Recursor. Lemma combine_length : forall (l:list A)(l':list B), length (combine l l') = min (length l) (length l'). Proof. - induction l. + intro l; induction l. simpl; auto. - destruct l'; simpl; auto. + intro l'; destruct l'; simpl; auto. Qed. 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). Proof. - induction l; destruct l'; intros; try discriminate. + intro l; induction l; intro l'; destruct l'; intros n x y; try discriminate. destruct n; simpl; auto. destruct n; simpl in *; auto. Qed. @@ -1826,7 +1829,7 @@ End Fold_Right_Recursor. forall (x:A) (y:B) (l:list B), In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). Proof. - induction l; + intros x y l; induction l; [ simpl; auto | simpl; destruct 1 as [H1| ]; [ left; rewrite H1; trivial | right; auto ] ]. @@ -1836,9 +1839,9 @@ End Fold_Right_Recursor. 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; + intro l; induction l; [ simpl; tauto - | simpl; intros; apply in_or_app; destruct H; + | simpl; intros l' x y H H0; apply in_or_app; destruct H as [H|H]; [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed. @@ -1846,10 +1849,10 @@ End Fold_Right_Recursor. 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. + intros l l' x y; split; [ | intros H; apply in_prod; intuition ]. + induction l as [|a l IHl]; simpl; intros H. intuition. - destruct (in_app_or _ _ _ H); clear H. + destruct (in_app_or _ _ _ H) as [H0|H0]; 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 as [= -> ->]; intuition. @@ -1859,7 +1862,7 @@ End Fold_Right_Recursor. Lemma prod_length : forall (l:list A)(l':list B), length (list_prod l l') = (length l) * (length l'). Proof. - induction l; simpl; auto. + intro l; induction l; simpl; auto. intros. rewrite app_length. rewrite map_length. @@ -1947,7 +1950,7 @@ Section SetIncl. Lemma incl_l_nil : forall l, incl l nil -> l = nil. Proof. - destruct l; intros Hincl. + intro l; destruct l as [|a l]; intros Hincl. - reflexivity. - exfalso; apply Hincl with a; simpl; auto. Qed. @@ -2021,7 +2024,7 @@ Section SetIncl. Lemma incl_app_inv : forall l1 l2 m : list A, incl (l1 ++ l2) m -> incl l1 m /\ incl l2 m. Proof. - induction l1; intros l2 m Hin; split; auto. + intro l1; induction l1 as [|a l1 IHl1]; intros l2 m Hin; split; auto. - apply incl_nil_l. - intros b Hb; inversion_clear Hb; subst; apply Hin. + now constructor. @@ -2083,9 +2086,9 @@ Section Cutting. 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|?]. + - intro l. inversion 1 as [H1|?]. rewrite (length_zero_iff_nil l) in H1. subst. now simpl. - - destruct l as [|x xs]; simpl. + - intro l; destruct l as [|x xs]; simpl. * now reflexivity. * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. Qed. @@ -2095,16 +2098,16 @@ Section Cutting. 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 | intro l; 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]. + Proof. intro l; induction l as [|x xs Hrec]. - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. - - destruct n. + - intro n; destruct n as [|n]. * now simpl. * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). Qed. @@ -2137,11 +2140,11 @@ Section Cutting. forall l:list A, forall i j : nat, firstn i (firstn j l) = firstn (min i j) l. - Proof. induction l as [|x xs Hl]. + Proof. intro l; induction l as [|x xs Hl]. - intros. simpl. now rewrite ?firstn_nil. - - destruct i. + - intro i; destruct i. * intro. now simpl. - * destruct j. + * intro j; destruct j. + now simpl. + simpl. f_equal. apply Hl. Qed. @@ -2157,11 +2160,11 @@ Section Cutting. Lemma firstn_skipn_comm : forall m n l, firstn m (skipn n l) = skipn n (firstn (n + m) l). - Proof. now intros m; induction n; intros []; simpl; destruct m. Qed. + Proof. now intros m n; induction n; intros []; simpl; destruct m. Qed. Lemma skipn_firstn_comm : forall m n l, skipn m (firstn n l) = firstn (n - m) (skipn m l). - Proof. now induction m; intros [] []; simpl; rewrite ?firstn_nil. Qed. + Proof. now intro m; induction m; intros [] []; simpl; rewrite ?firstn_nil. Qed. Lemma skipn_O : forall l, skipn 0 l = l. Proof. reflexivity. Qed. @@ -2173,7 +2176,7 @@ Section Cutting. Proof. reflexivity. Qed. Lemma skipn_all : forall l, skipn (length l) l = nil. - Proof. now induction l. Qed. + Proof. now intro l; induction l. Qed. #[deprecated(since="8.12",note="Use skipn_all instead.")] Notation skipn_none := skipn_all. @@ -2185,15 +2188,15 @@ Section Cutting. Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l. Proof. - induction n. + intro n; induction n. simpl; auto. - destruct l; simpl; auto. + intro l; destruct l; simpl; auto. f_equal; auto. Qed. Lemma firstn_length : forall n l, length (firstn n l) = min n (length l). Proof. - induction n; destruct l; simpl; auto. + intro n; induction n; intro l; destruct l; simpl; auto. Qed. Lemma skipn_length n : @@ -2201,7 +2204,7 @@ Section Cutting. Proof. induction n. - intros l; simpl; rewrite Nat.sub_0_r; reflexivity. - - destruct l; simpl; auto. + - intro l; destruct l; simpl; auto. Qed. Lemma skipn_app n : forall l1 l2, @@ -2241,11 +2244,11 @@ Section Cutting. Lemma removelast_firstn : forall n l, n < length l -> removelast (firstn (S n) l) = firstn n l. Proof. - induction n; destruct l. + intro n; induction n as [|n IHn]; intro l; destruct l as [|a l]. simpl; auto. simpl; auto. simpl; auto. - intros. + intros H. 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). @@ -2253,30 +2256,30 @@ Section Cutting. rewrite IHn; auto with arith. clear IHn; destruct l; simpl in *; try discriminate. - inversion_clear H. - inversion_clear H0. + inversion_clear H as [|? H1]. + inversion_clear H1. Qed. Lemma removelast_firstn_len : forall l, removelast l = firstn (pred (length l)) l. Proof. - induction l; [ reflexivity | simpl ]. + intro l; induction l as [|a l IHl]; [ reflexivity | simpl ]. destruct l; [ | rewrite IHl ]; reflexivity. Qed. Lemma firstn_removelast : forall n l, n < length l -> firstn n (removelast l) = firstn n l. Proof. - induction n; destruct l. + intro n; induction n; intro l; destruct l as [|a l]. simpl; auto. simpl; auto. simpl; auto. - intros. + intros H. simpl in H. 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. + intro H0; rewrite H0 in H; inversion_clear H as [|? H1]; inversion_clear H1. Qed. End Cutting. @@ -2300,9 +2303,9 @@ Section Combining. Lemma combine_firstn_l : forall (l : list A) (l' : list B), combine l l' = combine l (firstn (length l) l'). Proof. - induction l as [| x l IHl]; intros l'; [reflexivity|]. + intro l; induction l as [| x l IHl]; intros l'; [reflexivity|]. destruct l' as [| x' l']; [reflexivity|]. - simpl. specialize IHl with (l':=l'). rewrite <- IHl. + simpl. specialize IHl with l'. rewrite <- IHl. reflexivity. Qed. @@ -2313,14 +2316,14 @@ Section Combining. induction l' as [| x' l' IHl']; intros l. - simpl. apply combine_nil. - destruct l as [| x l]; [reflexivity|]. - simpl. specialize IHl' with (l:=l). rewrite <- IHl'. + simpl. specialize IHl' with l. rewrite <- IHl'. reflexivity. Qed. Lemma combine_firstn : forall (l : list A) (l' : list B) (n : nat), firstn n (combine l l') = combine (firstn n l) (firstn n l'). Proof. - induction l as [| x l IHl]; intros l' n. + intro l; induction l as [| x l IHl]; intros l' n. - simpl. repeat (rewrite firstn_nil). reflexivity. - destruct l' as [| x' l']. + simpl. repeat (rewrite firstn_nil). rewrite combine_nil. reflexivity. @@ -2353,7 +2356,7 @@ Section Add. Lemma Add_split a l l' : Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2. Proof. - induction 1. + induction 1 as [l|x ? ? ? IHAdd]. - exists nil; exists l; split; trivial. - destruct IHAdd as (l1 & l2 & Hl & Hl'). exists (x::l1); exists l2; split; simpl; f_equal; trivial. @@ -2362,7 +2365,7 @@ Section Add. 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 as [|? ? ? ? IHAdd]; intros; simpl in *; rewrite ?IHAdd; tauto. Qed. Lemma Add_length a l l' : Add a l l' -> length l' = S (length l). @@ -2437,7 +2440,7 @@ Section ReDun. Lemma NoDup_rev l : NoDup l -> NoDup (rev l). Proof. - induction l; simpl; intros Hnd; [ constructor | ]. + induction l as [|a l IHl]; simpl; intros Hnd; [ constructor | ]. inversion_clear Hnd as [ | ? ? Hnin Hndl ]. assert (Add a (rev l) (rev l ++ a :: nil)) as Hadd by (rewrite <- (app_nil_r (rev l)) at 1; apply Add_app). @@ -2447,10 +2450,10 @@ Section ReDun. Lemma NoDup_filter f l : NoDup l -> NoDup (filter f l). Proof. - induction l; simpl; intros Hnd; auto. + induction l as [|a l IHl]; simpl; intros Hnd; auto. apply NoDup_cons_iff in Hnd. destruct (f a); [ | intuition ]. - apply NoDup_cons_iff; split; intuition. + apply NoDup_cons_iff; split; [intro H|]; intuition. apply filter_In in H; intuition. Qed. @@ -2464,7 +2467,7 @@ Section ReDun. | x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs) end. - Lemma nodup_fixed_point : forall (l : list A), + Lemma nodup_fixed_point (l : list A) : NoDup l -> nodup l = l. Proof. induction l as [| x l IHl]; [auto|]. intros H. @@ -2512,7 +2515,7 @@ Section ReDun. - 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. - + split. + + intro H; split. * specialize (H a). rewrite count_occ_cons_eq in H; trivial. now inversion H. * intros x. specialize (H x). simpl in *. destruct (decA a x); auto. @@ -2547,7 +2550,7 @@ Section ReDun. * 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. + { induction l as [|a l IHl]; 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. @@ -2567,7 +2570,7 @@ Section ReDun. * 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. + { induction l as [|a l IHl]; 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. @@ -2591,7 +2594,7 @@ Section ReDun. 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]. - - destruct l'; easy. + - intro l'; 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. @@ -2604,7 +2607,7 @@ Section ReDun. Lemma NoDup_incl_NoDup (l l' : list A) : NoDup l -> length l' <= length l -> incl l l' -> NoDup l'. Proof. - revert l'; induction l; simpl; intros l' Hnd Hlen Hincl. + revert l'; induction l as [|a l IHl]; simpl; intros l' Hnd Hlen Hincl. - now destruct l'; inversion Hlen. - assert (In a l') as Ha by now apply Hincl; left. apply in_split in Ha as [l1' [l2' ->]]. @@ -2614,7 +2617,7 @@ Section ReDun. * rewrite app_length. rewrite app_length in Hlen; simpl in Hlen; rewrite Nat.add_succ_r in Hlen. now apply Nat.succ_le_mono. - * apply incl_Add_inv with (u:= l1' ++ l2') in Hincl; auto. + * apply (incl_Add_inv (u:= l1' ++ l2')) in Hincl; auto. apply Add_app. + intros Hnin'. assert (incl (a :: l) (l1' ++ l2')) as Hincl''. @@ -2663,13 +2666,13 @@ Section NatSeq. Lemma seq_length : forall len start, length (seq start len) = len. Proof. - induction len; simpl; auto. + intro len; induction len; simpl; auto. Qed. Lemma seq_nth : forall len start n d, n < len -> nth n (seq start len) d = start+n. Proof. - induction len; intros. + intro len; induction len as [|len IHlen]; intros start n d H. inversion H. simpl seq. destruct n; simpl. @@ -2680,7 +2683,7 @@ Section NatSeq. Lemma seq_shift : forall len start, map S (seq start len) = seq (S start) len. Proof. - induction len; simpl; auto. + intro len; induction len as [|len IHlen]; simpl; auto. intros. rewrite IHlen. auto with arith. @@ -2689,7 +2692,7 @@ Section NatSeq. Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len. Proof. - revert start. induction len; simpl; intros. + revert start. induction len as [|len IHlen]; 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. @@ -2706,7 +2709,7 @@ Section NatSeq. Lemma seq_app : forall len1 len2 start, seq start (len1 + len2) = seq start len1 ++ seq (start + len1) len2. Proof. - induction len1 as [|len1' IHlen]; intros; simpl in *. + intro len1; induction len1 as [|len1' IHlen]; intros; simpl in *. - now rewrite Nat.add_0_r. - now rewrite Nat.add_succ_r, IHlen. Qed. @@ -2751,7 +2754,7 @@ Section Exists_Forall. split. - intros HE; apply Exists_exists in HE. destruct HE as [a [Hin HP]]. - apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + apply (In_nth _ _ a) in Hin; destruct Hin as [i [Hl Heq]]. rewrite <- Heq in HP. now exists i; exists a. - intros [i [d [Hl HP]]]. @@ -2827,23 +2830,23 @@ Section Exists_Forall. Proof. split. - intros HF i d Hl. - apply Forall_forall with (x := nth i l d) in HF. + apply (Forall_forall l). assumption. apply nth_In; assumption. - intros HF. apply Forall_forall; intros a Hin. - apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + apply (In_nth _ _ a) in Hin; destruct Hin as [i [Hl Heq]]. rewrite <- Heq; intuition. Qed. Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a. Proof. - intros; inversion H; trivial. + intros a l H; inversion H; trivial. Qed. Theorem Forall_inv_tail : forall (a:A) l, Forall (a :: l) -> Forall l. Proof. - intros; inversion H; trivial. + intros a l H; inversion H; trivial. Qed. Lemma Forall_app l1 l2 : @@ -2868,14 +2871,14 @@ Section Exists_Forall. 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' l; 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}. Proof. - intro Pdec. induction l as [|a l' Hrec]. + intros Pdec l. induction l as [|a l' Hrec]. - left. apply Forall_nil. - destruct Hrec as [Hl'|Hl']. + destruct (Pdec a) as [Ha|Ha]. @@ -2894,7 +2897,7 @@ Section Exists_Forall. Proof. intros Hincl HF. apply Forall_forall; intros a Ha. - apply Forall_forall with (x:=a) in HF; intuition. + apply (Forall_forall l1); intuition. Qed. End One_predicate. @@ -2909,7 +2912,7 @@ Section Exists_Forall. forall l, Exists P l -> Exists Q l. Proof. intros P Q H l H0. - induction H0. + induction H0 as [x l H0|x l H0 IHExists]. apply (Exists_cons_hd Q x l (H x H0)). apply (Exists_cons_tl x IHExists). Qed. @@ -2917,7 +2920,7 @@ Section Exists_Forall. Lemma Exists_or : forall (P Q : A -> Prop) l, Exists P l \/ Exists Q l -> Exists (fun x => P x \/ Q x) l. Proof. - induction l; intros [H | H]; inversion H; subst. + intros P Q l; induction l as [|a l IHl]; intros [H | H]; inversion H; subst. 1,3: apply Exists_cons_hd; auto. all: apply Exists_cons_tl, IHl; auto. Qed. @@ -2925,7 +2928,8 @@ Section Exists_Forall. Lemma Exists_or_inv : forall (P Q : A -> Prop) l, Exists (fun x => P x \/ Q x) l -> Exists P l \/ Exists Q l. Proof. - induction l; intro Hl; inversion Hl as [ ? ? H | ? ? H ]; subst. + intros P Q l; induction l as [|a l IHl]; + intro Hl; inversion Hl as [ ? ? H | ? ? H ]; subst. - inversion H; now repeat constructor. - destruct (IHl H); now repeat constructor. Qed. @@ -2939,13 +2943,13 @@ Section Exists_Forall. Lemma Forall_and : forall (P Q : A -> Prop) l, Forall P l -> Forall Q l -> Forall (fun x => P x /\ Q x) l. Proof. - induction l; intros HP HQ; constructor; inversion HP; inversion HQ; auto. + intros P Q l; induction l; intros HP HQ; constructor; inversion HP; inversion HQ; auto. Qed. Lemma Forall_and_inv : forall (P Q : A -> Prop) l, Forall (fun x => P x /\ Q x) l -> Forall P l /\ Forall Q l. Proof. - induction l; intro Hl; split; constructor; inversion Hl; firstorder. + intros P Q l; induction l; intro Hl; split; constructor; inversion Hl; firstorder. Qed. Lemma Forall_Exists_neg (P:A->Prop)(l:list A) : @@ -2975,7 +2979,7 @@ Section Exists_Forall. Exists (fun x => ~ P x) l. Proof. intro Dec. - apply Exists_Forall_neg; intros. + apply Exists_Forall_neg; intros x. destruct (Dec x); auto. Qed. @@ -3001,7 +3005,7 @@ Hint Constructors Forall : core. Lemma exists_Forall A B : forall (P : A -> B -> Prop) l, (exists k, Forall (P k) l) -> Forall (fun x => exists k, P k x) l. Proof. - induction l; intros [k HF]; constructor; inversion_clear HF. + intros P l; induction l as [|a l IHl]; intros [k HF]; constructor; inversion_clear HF. - now exists k. - now apply IHl; exists k. Qed. @@ -3009,7 +3013,7 @@ Qed. Lemma Forall_image A B : forall (f : A -> B) l, Forall (fun y => exists x, y = f x) l <-> exists l', l = map f l'. Proof. - induction l; split; intros HF. + intros f l; induction l as [|a l IHl]; split; intros HF. - exists nil; reflexivity. - constructor. - inversion_clear HF as [| ? ? [x Hx] HFtl]; subst. @@ -3026,7 +3030,7 @@ Qed. Lemma concat_nil_Forall A : forall (l : list (list A)), concat l = nil <-> Forall (fun x => x = nil) l. Proof. - induction l; simpl; split; intros Hc; auto. + intro l; induction l as [|a l IHl]; simpl; split; intros Hc; auto. - apply app_eq_nil in Hc. constructor; firstorder. - inversion Hc; subst; simpl. @@ -3069,9 +3073,9 @@ Section Forall2. Forall2 (l1 ++ l2) l' -> exists l1' l2', Forall2 l1 l1' /\ Forall2 l2 l2' /\ l' = l1' ++ l2'. Proof. - induction l1; intros. + intro l1; induction l1 as [|a l1 IHl1]; intros l2 l' H. exists [], l'; auto. - simpl in H; inversion H; subst; clear H. + simpl in H; inversion H as [|? y ? ? ? H4]; subst; clear H. apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->). exists (y::l1'), l2'; simpl; auto. Qed. @@ -3080,9 +3084,9 @@ Section Forall2. Forall2 l (l1' ++ l2') -> exists l1 l2, Forall2 l1 l1' /\ Forall2 l2 l2' /\ l = l1 ++ l2. Proof. - induction l1'; intros. + intro l1'; induction l1' as [|a l1' IHl1']; intros l2' l H. exists [], l; auto. - simpl in H; inversion H; subst; clear H. + simpl in H; inversion H as [|x ? ? ? ? H4]; subst; clear H. apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->). exists (x::l1), l2; simpl; auto. Qed. @@ -3090,7 +3094,7 @@ Section Forall2. 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 l1 l2 l1' l2' H H0. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto. Qed. End Forall2. @@ -3133,7 +3137,7 @@ Section ForallPairs. Lemma ForallPairs_ForallOrdPairs l: ForallPairs l -> ForallOrdPairs l. Proof. - induction l; auto. intros H. + induction l as [|a l IHl]; auto. intros H. constructor. apply <- Forall_forall. intros; apply H; simpl; auto. apply IHl. red; intros; apply H; simpl; auto. @@ -3173,7 +3177,7 @@ Section Repeat. Lemma repeat_cons n a : a :: repeat a n = repeat a n ++ (a :: nil). Proof. - induction n; simpl. + induction n as [|n IHn]; simpl. - reflexivity. - f_equal; apply IHn. Qed. @@ -3221,7 +3225,7 @@ End Repeat. Lemma repeat_to_concat A n (a:A) : repeat a n = concat (repeat [a] n). Proof. - induction n; simpl. + induction n as [|n IHn]; simpl. - reflexivity. - f_equal; apply IHn. Qed. @@ -3234,7 +3238,7 @@ Definition list_sum l := fold_right plus 0 l. Lemma list_sum_app : forall l1 l2, list_sum (l1 ++ l2) = list_sum l1 + list_sum l2. Proof. -induction l1; intros l2; [ reflexivity | ]. +intro l1; induction l1 as [|a l1 IHl1]; intros l2; [ reflexivity | ]. simpl; rewrite IHl1. apply Nat.add_assoc. Qed. @@ -3246,14 +3250,14 @@ Definition list_max l := fold_right max 0 l. Lemma list_max_app : forall l1 l2, list_max (l1 ++ l2) = max (list_max l1) (list_max l2). Proof. -induction l1; intros l2; [ reflexivity | ]. +intro l1; induction l1 as [|a l1 IHl1]; intros l2; [ reflexivity | ]. now simpl; rewrite IHl1, Nat.max_assoc. Qed. Lemma list_max_le : forall l n, list_max l <= n <-> Forall (fun k => k <= n) l. Proof. -induction l; simpl; intros n; split; intros H; intuition. +intro l; induction l as [|a l IHl]; simpl; intros n; split; intros H; intuition. - apply Nat.max_lub_iff in H. now constructor; [ | apply IHl ]. - inversion_clear H as [ | ? ? Hle HF ]. @@ -3263,7 +3267,7 @@ Qed. Lemma list_max_lt : forall l n, l <> nil -> list_max l < n <-> Forall (fun k => k < n) l. Proof. -induction l; simpl; intros n Hnil; split; intros H; intuition. +intro l; induction l as [|a l IHl]; simpl; intros n Hnil; split; intros H; intuition. - destruct l. + repeat constructor. now simpl in H; rewrite Nat.max_0_r in H. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 23d486ff90..a918d1ecd7 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -104,7 +104,7 @@ Section Dependent_Equality. Lemma eq_dep_dep1 : forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y. Proof. - destruct 1. + intros p; destruct 1. apply eq_dep1_intro with (eq_refl p). simpl; trivial. Qed. @@ -120,7 +120,7 @@ Lemma eq_sigT_eq_dep : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), existT P p x = existT P q y -> eq_dep p x q y. Proof. - intros. + intros * H. dependent rewrite H. apply eq_dep_intro. Qed. @@ -145,7 +145,7 @@ Lemma eq_sig_eq_dep : forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q), exist P p x = exist P q y -> eq_dep p x q y. Proof. - intros. + intros * H. dependent rewrite H. apply eq_dep_intro. Qed. @@ -168,10 +168,10 @@ Qed. Set Implicit Arguments. -Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> - {H:x1=x2 | rew H in H1 = H2}. +Lemma eq_sigT_sig_eq X P (x1 x2:X) H1 H2 : + existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}. Proof. - intros; split; intro H. + split; intro H. - change x2 with (projT1 (existT P x2 H2)). change H2 with (projT2 (existT P x2 H2)) at 5. destruct H. simpl. @@ -181,19 +181,17 @@ Proof. reflexivity. Defined. -Lemma eq_sigT_fst : - forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), x1 = x2. +Lemma eq_sigT_fst X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2) : + x1 = x2. Proof. - intros. change x2 with (projT1 (existT P x2 H2)). destruct H. reflexivity. Defined. -Lemma eq_sigT_snd : - forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2. +Lemma eq_sigT_snd X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2) : + rew (eq_sigT_fst H) in H1 = H2. Proof. - intros. unfold eq_sigT_fst. change x2 with (projT1 (existT P x2 H2)). change H2 with (projT2 (existT P x2 H2)) at 3. @@ -201,19 +199,17 @@ Proof. reflexivity. Defined. -Lemma eq_sig_fst : - forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), x1 = x2. +Lemma eq_sig_fst X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2) : + x1 = x2. Proof. - intros. change x2 with (proj1_sig (exist P x2 H2)). destruct H. reflexivity. Defined. -Lemma eq_sig_snd : - forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2. +Lemma eq_sig_snd X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2) : + rew (eq_sig_fst H) in H1 = H2. Proof. - intros. unfold eq_sig_fst, eq_ind. change x2 with (proj1_sig (exist P x2 H2)). change H2 with (proj2_sig (exist P x2 H2)) at 3. @@ -283,7 +279,7 @@ Section Equivalences. Lemma eq_rect_eq_on__eq_dep_eq_on (p : U) (P : U -> Type) (x : P p) : Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x. Proof. - intros eq_rect_eq; red; intros. + intros eq_rect_eq; red; intros y H. symmetry; apply (eq_rect_eq_on__eq_dep1_eq_on _ _ _ eq_rect_eq). apply eq_dep_sym in H; apply eq_dep_dep1; trivial. Qed. @@ -299,7 +295,7 @@ Section Equivalences. Proof. intro eq_dep_eq; red. elim p1 using eq_indd. - intros; apply eq_dep_eq. + intros p2; apply eq_dep_eq. elim p2 using eq_indd. apply eq_dep_intro. Qed. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 6ef5fa7d4c..4af90ae12d 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -46,9 +46,8 @@ Section EqdepDec. Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' := eq_ind _ (fun a => a = y') eq2 _ eq1. - Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = eq_refl y. + Remark trans_sym_eq (x y:A) (u:x = y) : comp u u = eq_refl y. Proof. - intros. case u; trivial. Qed. @@ -62,8 +61,7 @@ Section EqdepDec. | or_intror neqxy => False_ind _ (neqxy u) end. - Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v. - intros. + Let nu_constant (y:A) (u v:x = y) : nu u = nu v. unfold nu. destruct (eq_dec y) as [Heq|Hneq]. - reflexivity. @@ -75,27 +73,23 @@ Section EqdepDec. Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (eq_refl x)) v. - Remark nu_left_inv_on : forall (y:A) (u:x = y), nu_inv (nu u) = u. + Remark nu_left_inv_on (y:A) (u:x = y) : nu_inv (nu u) = u. Proof. - intros. case u; unfold nu_inv. apply trans_sym_eq. Qed. - Theorem eq_proofs_unicity_on : forall (y:A) (p1 p2:x = y), p1 = p2. + Theorem eq_proofs_unicity_on (y:A) (p1 p2:x = y) : p1 = p2. Proof. - intros. - elim nu_left_inv_on with (u := p1). - elim nu_left_inv_on with (u := p2). + elim (nu_left_inv_on p1). + elim (nu_left_inv_on p2). elim nu_constant with y p1 p2. reflexivity. Qed. - Theorem K_dec_on : - forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p. + Theorem K_dec_on (P:x = x -> Prop) (H:P (eq_refl x)) (p:x = x) : P p. Proof. - intros. elim eq_proofs_unicity_on with x (eq_refl x) p. trivial. Qed. @@ -112,11 +106,10 @@ Section EqdepDec. end. - Theorem inj_right_pair_on : - forall (P:A -> Prop) (y y':P x), - ex_intro P x y = ex_intro P x y' -> y = y'. + Theorem inj_right_pair_on (P:A -> Prop) (y y':P x) : + ex_intro P x y = ex_intro P x y' -> y = y'. Proof. - intros. + intros H. cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y). - simpl. destruct (eq_dec x) as [Heq|Hneq]. @@ -156,14 +149,11 @@ Proof (@inj_right_pair_on A x (eq_dec x)). Require Import EqdepFacts. (** We deduce axiom [K] for (decidable) types *) -Theorem K_dec_type : - forall A:Type, - (forall x y:A, {x = y} + {x <> y}) -> - forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p. +Theorem K_dec_type (A:Type) (eq_dec:forall x y:A, {x = y} + {x <> y}) (x:A) + (P:x = x -> Prop) (H:P (eq_refl x)) (p:x = x) : P p. Proof. - intros A eq_dec x P H p. - elim p using K_dec; intros. - - case (eq_dec x0 y); [left|right]; assumption. + elim p using K_dec. + - intros x0 y; case (eq_dec x0 y); [left|right]; assumption. - trivial. Qed. @@ -259,7 +249,7 @@ Module DecidableEqDep (M:DecidableType). ex_intro P x p = ex_intro P x q -> p = q. Proof. intros. - apply inj_right_pair with (A:=U). + apply inj_right_pair. - intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption. - assumption. Qed. @@ -377,7 +367,7 @@ Defined. Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl. Proof. - induction n. + induction n as [|n IHn]. - change (match 0 as n return 0=n -> Prop with | 0 => fun x => x = eq_refl | _ => fun _ => True diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 28ba9daed0..039e920c29 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -94,7 +94,7 @@ Defined. Definition discr n : { p:positive | n = pos p } + { n = 0 }. Proof. - destruct n; auto. + destruct n as [|p]; auto. left; exists p; auto. Defined. @@ -486,7 +486,7 @@ Qed. Lemma size_le n : 2^(size n) <= succ_double n. Proof. - destruct n. discriminate. simpl. + destruct n as [|p]. discriminate. simpl. change (2^Pos.size p <= Pos.succ (p~0))%positive. apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le. Qed. @@ -512,10 +512,10 @@ Qed. Lemma even_spec n : even n = true <-> Even n. Proof. - destruct n. + destruct n as [|p]. split. now exists 0. trivial. - destruct p; simpl; split; try easy. + destruct p as [p|p|]; simpl; split; try easy. intros (m,H). now destruct m. now exists (pos p). intros (m,H). now destruct m. @@ -523,10 +523,10 @@ Qed. Lemma odd_spec n : odd n = true <-> Odd n. Proof. - destruct n. + destruct n as [|p]. split. discriminate. intros (m,H). now destruct m. - destruct p; simpl; split; try easy. + destruct p as [p|p|]; simpl; split; try easy. now exists (pos p). intros (m,H). now destruct m. now exists 0. @@ -537,7 +537,8 @@ Qed. Theorem pos_div_eucl_spec (a:positive)(b:N) : let (q,r) := pos_div_eucl a b in pos a = q * b + r. Proof. - induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. + induction a as [a IHa|a IHa|]; + cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. (* a~1 *) destruct pos_div_eucl as (q,r). change (pos a~1) with (succ_double (pos a)). @@ -579,7 +580,8 @@ Theorem pos_div_eucl_remainder (a:positive) (b:N) : b<>0 -> snd (pos_div_eucl a b) < b. Proof. intros Hb. - induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. + induction a as [a IHa|a IHa|]; + cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. (* a~1 *) destruct pos_div_eucl as (q,r); simpl in *. case leb_spec; intros H; simpl; trivial. @@ -612,7 +614,7 @@ Qed. Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n. Proof. - destruct n. reflexivity. + destruct n as [|p]. reflexivity. unfold sqrtrem, sqrt, Pos.sqrt. destruct (Pos.sqrtrem p) as (s,r). now destruct r. Qed. @@ -620,7 +622,7 @@ Qed. Lemma sqrtrem_spec n : let (s,r) := sqrtrem n in n = s*s + r /\ r <= 2*s. Proof. - destruct n. now split. + destruct n as [|p]. now split. generalize (Pos.sqrtrem_spec p). simpl. destruct 1; simpl; subst; now split. Qed. @@ -628,7 +630,7 @@ Qed. Lemma sqrt_spec n : 0<=n -> let s := sqrt n in s*s <= n < (succ s)*(succ s). Proof. - intros _. destruct n. now split. apply (Pos.sqrt_spec p). + intros _. destruct n as [|p]. now split. apply (Pos.sqrt_spec p). Qed. Lemma sqrt_neg n : n<0 -> sqrt n = 0. @@ -749,7 +751,7 @@ Lemma shiftr_spec a n m : 0<=m -> testbit (shiftr a n) m = testbit a (m+n). Proof. intros _. revert a m. - induction n using peano_ind; intros a m. now rewrite add_0_r. + induction n as [|n IHn] using peano_ind; intros a m. now rewrite add_0_r. rewrite add_comm, add_succ_l, add_comm, <- add_succ_l. now rewrite <- IHn, testbit_succ_r_div2, shiftr_succ_r by apply le_0_l. Qed. @@ -771,10 +773,10 @@ Lemma shiftl_spec_low a n m : m<n -> testbit (shiftl a n) m = false. Proof. revert a m. - induction n using peano_ind; intros a m H. + induction n as [|n IHn] using peano_ind; intros a m H. elim (le_0_l m). now rewrite compare_antisym, H. rewrite shiftl_succ_r. - destruct m. now destruct (shiftl a n). + destruct m as [|p]. now destruct (shiftl a n). rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l. apply IHn. apply add_lt_mono_l with 1. rewrite 2 (add_succ_l 0). simpl. @@ -902,8 +904,8 @@ Qed. Lemma pos_pred_shiftl_low : forall p n m, m<n -> testbit (Pos.pred_N (Pos.shiftl p n)) m = true. Proof. - induction n using peano_ind. - now destruct m. + intros p n; induction n as [|n IHn] using peano_ind. + now intro m; destruct m. intros m H. unfold Pos.shiftl. destruct n as [|n]; simpl in *. destruct m. now destruct p. elim (Pos.nlt_1_r _ H). @@ -921,7 +923,7 @@ Lemma pos_pred_shiftl_high : forall p n m, n<=m -> testbit (Pos.pred_N (Pos.shiftl p n)) m = testbit (shiftl (Pos.pred_N p) n) m. Proof. - induction n using peano_ind; intros m H. + intros p n; induction n as [|n IHn] using peano_ind; intros m H. unfold shiftl. simpl. now destruct (Pos.pred_N p). rewrite shiftl_succ_r. destruct n as [|n]. @@ -945,11 +947,11 @@ Qed. (** ** Properties of [iter] *) -Lemma iter_swap_gen : forall A B (f:A -> B) (g:A -> A) (h:B -> B), +Lemma iter_swap_gen A B (f:A -> B) (g:A -> A) (h:B -> B) : (forall a, f (g a) = h (f a)) -> forall n a, f (iter n g a) = iter n h (f a). Proof. - destruct n; simpl; intros; rewrite ?H; trivial. + intros H n; destruct n; simpl; intros; rewrite ?H; trivial. now apply Pos.iter_swap_gen. Qed. @@ -964,7 +966,7 @@ Theorem iter_succ : forall n (A:Type) (f:A -> A) (x:A), iter (succ n) f x = f (iter n f x). Proof. - destruct n; intros; simpl; trivial. + intro n; destruct n; intros; simpl; trivial. now apply Pos.iter_succ. Qed. @@ -979,17 +981,16 @@ Theorem iter_add : forall p q (A:Type) (f:A -> A) (x:A), iter (p+q) f x = iter p f (iter q f x). Proof. - induction p using peano_ind; intros; trivial. + intro p; induction p as [|p IHp] using peano_ind; intros; trivial. now rewrite add_succ_l, !iter_succ, IHp. Qed. -Theorem iter_ind : - forall (A:Type) (f:A -> A) (a:A) (P:N -> A -> Prop), +Theorem iter_ind (A:Type) (f:A -> A) (a:A) (P:N -> A -> Prop) : P 0 a -> (forall n a', P n a' -> P (succ n) (f a')) -> forall n, P n (iter n f a). Proof. - induction n using peano_ind; trivial. + intros ? ? n; induction n using peano_ind; trivial. rewrite iter_succ; auto. Qed. @@ -998,7 +999,7 @@ Theorem iter_invariant : (forall x:A, Inv x -> Inv (f x)) -> forall x:A, Inv x -> Inv (iter n f x). Proof. - intros; apply iter_ind with (P := fun _ => Inv); trivial. + intros; apply iter_ind; trivial. Qed. End N. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 43fa8516d3..48df5fe884 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -70,7 +70,7 @@ Lemma inj_sub a a' : N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial. - destruct (Pos.compare_spec a a'). + destruct (Pos.compare_spec a a') as [H|H|H]. - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag. - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl. @@ -93,8 +93,8 @@ Qed. Lemma inj_compare a a' : (a ?= a')%N = (N.to_nat a ?= N.to_nat a'). Proof. - destruct a, a'; simpl; trivial. - - now destruct (Pos2Nat.is_succ p) as (n,->). + destruct a as [|p], a' as [|p']; simpl; trivial. + - now destruct (Pos2Nat.is_succ p') as (n,->). - now destruct (Pos2Nat.is_succ p) as (n,->). - apply Pos2Nat.inj_compare. Qed. diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 8c4d072114..55c4b193a5 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -58,7 +58,7 @@ Qed. Theorem succ_add_discr : forall n m, m ~= S (n + m). Proof. -intro n; induct m. +intros n m; induct m. apply neq_sym. apply neq_succ_0. intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. unfold not in IH; now apply IH. diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 7c74de6364..d0ef94d1a4 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -19,7 +19,7 @@ Include NOrderProp N. Theorem le_add_r : forall n m, n <= n + m. Proof. -intro n; induct m. +intros n m; induct m. rewrite add_0_r; now apply eq_le_incl. intros m IH. rewrite add_succ_r; now apply le_le_succ_r. Qed. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index a141cb7c0d..185a5974c2 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -39,7 +39,7 @@ Qed. Theorem le_0_l : forall n, 0 <= n. Proof. -nzinduct n. +intro n; nzinduct n. now apply eq_le_incl. intro n; split. apply le_le_succ_r. @@ -79,21 +79,21 @@ Proof. intro H; apply (neq_succ_0 0). apply H. Qed. -Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m. +Theorem neq_0_r n : n ~= 0 <-> exists m, n == S m. Proof. cases n. split; intro H; [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0]. intro n; split; intro H; [now exists n | apply neq_succ_0]. Qed. -Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m. +Theorem zero_or_succ n : n == 0 \/ exists m, n == S m. Proof. cases n. now left. intro n; right; now exists n. Qed. -Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1. +Theorem eq_pred_0 n : P n == 0 <-> n == 0 \/ n == 1. Proof. cases n. rewrite pred_0. now split; [left|]. @@ -103,16 +103,16 @@ intros [H|H]. elim (neq_succ_0 _ H). apply succ_inj_wd. now rewrite <- one_succ. Qed. -Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n. +Theorem succ_pred n : n ~= 0 -> S (P n) == n. Proof. cases n. intro H; exfalso; now apply H. intros; now rewrite pred_succ. Qed. -Theorem pred_inj : forall n m, n ~= 0 -> m ~= 0 -> P n == P m -> n == m. +Theorem pred_inj n m : n ~= 0 -> m ~= 0 -> P n == P m -> n == m. Proof. -intros n m; cases n. +cases n. intros H; exfalso; now apply H. intros n _; cases m. intros H; exfalso; now apply H. @@ -134,7 +134,7 @@ Proof. rewrite one_succ. intros until 3. assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))]. -induct n; [ | intros n [IH1 IH2]]; auto. +intro n; induct n; [ | intros n [IH1 IH2]]; auto. Qed. End PairInduction. @@ -151,10 +151,10 @@ Theorem two_dim_induction : (forall n m, R n m -> R n (S m)) -> (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m. Proof. -intros H1 H2 H3. induct n. -induct m. +intros H1 H2 H3. intro n; induct n. +intro m; induct m. exact H1. exact (H2 0). -intros n IH. induct m. +intros n IH. intro m; induct m. now apply H3. exact (H2 (S n)). Qed. @@ -171,8 +171,8 @@ Theorem double_induction : (forall n, R (S n) 0) -> (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m. Proof. -intros H1 H2 H3; induct n; auto. -intros n H; cases m; auto. +intros H1 H2 H3 n; induct n; auto. +intros n H m; cases m; auto. Qed. End DoubleInduction. diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 6e557a567e..313b9adfd1 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -190,7 +190,7 @@ Qed. Lemma bit0_odd : forall a, a.[0] = odd a. Proof. - intros. symmetry. + intros a. symmetry. destruct (exists_div2 a) as (a' & b & EQ). rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2. destruct b; simpl; apply odd_1 || apply odd_0. @@ -272,14 +272,14 @@ Qed. Lemma mul_pow2_bits_high : forall a n m, n<=m -> (a*2^n).[m] = a.[m-n]. Proof. - intros. + intros a n m ?. rewrite <- (sub_add n m) at 1 by order'. now rewrite mul_pow2_bits_add. Qed. Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false. Proof. - intros. apply testbit_false. + intros a n m H. apply testbit_false. rewrite <- (sub_add m n) by order'. rewrite pow_add_r, mul_assoc. rewrite div_mul by order_nz. rewrite <- (succ_pred (n-m)). rewrite pow_succ_r. @@ -370,7 +370,10 @@ Qed. Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. -Ltac bitwise := apply bits_inj; intros ?m; autorewrite with bitwise. +Tactic Notation "bitwise" "as" simple_intropattern(m) + := apply bits_inj; intros m; autorewrite with bitwise. + +Ltac bitwise := bitwise as ?m. (** The streams of bits that correspond to a natural numbers are exactly the ones that are always 0 after some point *) @@ -418,7 +421,7 @@ Qed. Lemma shiftl_mul_pow2 : forall a n, a << n == a * 2^n. Proof. - intros. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m) as [H|H]. now rewrite shiftl_spec_high', mul_pow2_bits_high. now rewrite shiftl_spec_low, mul_pow2_bits_low. @@ -455,7 +458,7 @@ Qed. Lemma shiftr_shiftl_l : forall a n m, m<=n -> (a << n) >> m == a << (n-m). Proof. - intros. + intros a n m ?. rewrite shiftr_div_pow2, !shiftl_mul_pow2. rewrite <- (sub_add m n) at 1 by trivial. now rewrite pow_add_r, mul_assoc, div_mul by order_nz. @@ -464,7 +467,7 @@ Qed. Lemma shiftr_shiftl_r : forall a n m, n<=m -> (a << n) >> m == a >> (m-n). Proof. - intros. + intros a n m ?. rewrite !shiftr_div_pow2, shiftl_mul_pow2. rewrite <- (sub_add n m) at 1 by trivial. rewrite pow_add_r, (mul_comm (2^(m-n))). @@ -630,7 +633,7 @@ Qed. Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0. Proof. - intros a b H. bitwise. + intros a b H. bitwise as m. apply (orb_false_iff a.[m] b.[m]). now rewrite <- lor_spec, H, bits_0. Qed. @@ -638,7 +641,7 @@ Qed. Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0. Proof. intros a b. split. - split. now apply lor_eq_0_l in H. + intro H; split. now apply lor_eq_0_l in H. rewrite lor_comm in H. now apply lor_eq_0_l in H. intros (EQ,EQ'). now rewrite EQ, lor_0_l. Qed. @@ -751,13 +754,13 @@ Proof. unfold clearbit. solve_proper. Qed. Lemma pow2_bits_true : forall n, (2^n).[n] = true. Proof. - intros. rewrite <- (mul_1_l (2^n)). rewrite <- (add_0_l n) at 2. + intros n. rewrite <- (mul_1_l (2^n)). rewrite <- (add_0_l n) at 2. now rewrite mul_pow2_bits_add, bit0_odd, odd_1. Qed. Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false. Proof. - intros. + intros n m ?. rewrite <- (mul_1_l (2^n)). destruct (le_gt_cases n m). rewrite mul_pow2_bits_high; trivial. @@ -768,7 +771,7 @@ Qed. Lemma pow2_bits_eqb : forall n m, (2^n).[m] = eqb n m. Proof. - intros. apply eq_true_iff_eq. rewrite eqb_eq. split. + intros n m. apply eq_true_iff_eq. rewrite eqb_eq. split. destruct (eq_decidable n m) as [H|H]. trivial. now rewrite (pow2_bits_false _ _ H). intros EQ. rewrite EQ. apply pow2_bits_true. @@ -813,7 +816,7 @@ Qed. Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false. Proof. - intros. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). + intros a n. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). apply andb_false_r. Qed. @@ -830,7 +833,7 @@ Qed. Lemma shiftl_lxor : forall a b n, (lxor a b) << n == lxor (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', lxor_spec. now rewrite !shiftl_spec_low. @@ -845,7 +848,7 @@ Qed. Lemma shiftl_land : forall a b n, (land a b) << n == land (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', land_spec. now rewrite !shiftl_spec_low. @@ -860,7 +863,7 @@ Qed. Lemma shiftl_lor : forall a b n, (lor a b) << n == lor (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', lor_spec. now rewrite !shiftl_spec_low. @@ -875,7 +878,7 @@ Qed. Lemma shiftl_ldiff : forall a b n, (ldiff a b) << n == ldiff (a << n) (b << n). Proof. - intros. bitwise. + intros a b n. bitwise as m. destruct (le_gt_cases n m). now rewrite !shiftl_spec_high', ldiff_spec. now rewrite !shiftl_spec_low. @@ -944,7 +947,7 @@ Qed. Lemma ones_spec_high : forall n m, n<=m -> (ones n).[m] = false. Proof. - intros. + intros n m ?. destruct (eq_0_gt_0_cases n) as [EQ|LT]; rewrite ones_equiv. now rewrite EQ, pow_0_r, one_succ, pred_succ, bits_0. apply bits_above_log2. @@ -973,7 +976,7 @@ Qed. Lemma lnot_involutive : forall a n, lnot (lnot a n) n == a. Proof. - intros a n. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m). now rewrite 2 lnot_spec_high. now rewrite 2 lnot_spec_low, negb_involutive. @@ -994,7 +997,7 @@ Qed. Lemma lor_ones_low : forall a n, log2 a < n -> lor a (ones n) == ones n. Proof. - intros a n H. bitwise. destruct (le_gt_cases n m). + intros a n H. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. now rewrite ones_spec_low, orb_true_r. @@ -1002,7 +1005,7 @@ Qed. Lemma land_ones : forall a n, land a (ones n) == a mod 2^n. Proof. - intros a n. bitwise. destruct (le_gt_cases n m). + intros a n. bitwise as m. destruct (le_gt_cases n m). now rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r. now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r. Qed. @@ -1017,7 +1020,7 @@ Qed. Lemma ldiff_ones_r : forall a n, ldiff a (ones n) == (a >> n) << n. Proof. - intros a n. bitwise. destruct (le_gt_cases n m). + intros a n. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, shiftl_spec_high', shiftr_spec'; trivial. rewrite sub_add; trivial. apply andb_true_r. now rewrite ones_spec_low, shiftl_spec_low, andb_false_r. @@ -1026,7 +1029,7 @@ Qed. Lemma ldiff_ones_r_low : forall a n, log2 a < n -> ldiff a (ones n) == 0. Proof. - intros a n H. bitwise. destruct (le_gt_cases n m). + intros a n H. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. now rewrite ones_spec_low, andb_false_r. @@ -1035,7 +1038,7 @@ Qed. Lemma ldiff_ones_l_low : forall a n, log2 a < n -> ldiff (ones n) a == lnot a n. Proof. - intros a n H. bitwise. destruct (le_gt_cases n m). + intros a n H. bitwise as m. destruct (le_gt_cases n m). rewrite ones_spec_high, lnot_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. now rewrite ones_spec_low, lnot_spec_low. @@ -1044,7 +1047,7 @@ Qed. Lemma lor_lnot_diag : forall a n, lor a (lnot a n) == lor a (ones n). Proof. - intros a n. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m). rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m]. rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m]. @@ -1059,7 +1062,7 @@ Qed. Lemma land_lnot_diag : forall a n, land a (lnot a n) == ldiff a (ones n). Proof. - intros a n. bitwise. + intros a n. bitwise as m. destruct (le_gt_cases n m). rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m]. rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m]. @@ -1074,7 +1077,7 @@ Qed. Lemma lnot_lor_low : forall a b n, log2 a < n -> log2 b < n -> lnot (lor a b) n == land (lnot a n) (lnot b n). Proof. - intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + intros a b n Ha Hb. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, lor_spec, !bits_above_log2; trivial. now apply lt_le_trans with n. now apply lt_le_trans with n. @@ -1084,7 +1087,7 @@ Qed. Lemma lnot_land_low : forall a b n, log2 a < n -> log2 b < n -> lnot (land a b) n == lor (lnot a n) (lnot b n). Proof. - intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + intros a b n Ha Hb. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, land_spec, !bits_above_log2; trivial. now apply lt_le_trans with n. now apply lt_le_trans with n. @@ -1094,7 +1097,7 @@ Qed. Lemma ldiff_land_low : forall a b n, log2 a < n -> ldiff a b == land a (lnot b n). Proof. - intros a b n Ha. bitwise. destruct (le_gt_cases n m). + intros a b n Ha. bitwise as m. destruct (le_gt_cases n m). rewrite (bits_above_log2 a m). trivial. now apply lt_le_trans with n. rewrite !lnot_spec_low; trivial. @@ -1103,7 +1106,7 @@ Qed. Lemma lnot_ldiff_low : forall a b n, log2 a < n -> log2 b < n -> lnot (ldiff a b) n == lor (lnot a n) b. Proof. - intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + intros a b n Ha Hb. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, ldiff_spec, !bits_above_log2; trivial. now apply lt_le_trans with n. now apply lt_le_trans with n. @@ -1113,7 +1116,7 @@ Qed. Lemma lxor_lnot_lnot : forall a b n, lxor (lnot a n) (lnot b n) == lxor a b. Proof. - intros a b n. bitwise. destruct (le_gt_cases n m). + intros a b n. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high; trivial. rewrite !lnot_spec_low, xorb_negb_negb; trivial. Qed. @@ -1121,7 +1124,7 @@ Qed. Lemma lnot_lxor_l : forall a b n, lnot (lxor a b) n == lxor (lnot a n) b. Proof. - intros a b n. bitwise. destruct (le_gt_cases n m). + intros a b n. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, lxor_spec; trivial. rewrite !lnot_spec_low, lxor_spec, negb_xorb_l; trivial. Qed. @@ -1129,7 +1132,7 @@ Qed. Lemma lnot_lxor_r : forall a b n, lnot (lxor a b) n == lxor a (lnot b n). Proof. - intros a b n. bitwise. destruct (le_gt_cases n m). + intros a b n. bitwise as m. destruct (le_gt_cases n m). rewrite !lnot_spec_high, lxor_spec; trivial. rewrite !lnot_spec_low, lxor_spec, negb_xorb_r; trivial. Qed. @@ -1137,7 +1140,7 @@ Qed. Lemma lxor_lor : forall a b, land a b == 0 -> lxor a b == lor a b. Proof. - intros a b H. bitwise. + intros a b H. bitwise as m. assert (a.[m] && b.[m] = false) by now rewrite <- land_spec, H, bits_0. now destruct a.[m], b.[m]. @@ -1264,7 +1267,7 @@ Qed. Lemma add_carry_div2 : forall a b (c0:bool), (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0. Proof. - intros. + intros a b c0. rewrite <- add3_bits_div2. rewrite (add_comm ((a/2)+_)). rewrite <- div_add by order'. @@ -1312,7 +1315,7 @@ Proof. apply div_lt_upper_bound; trivial. order'. now rewrite <- pow_succ_r'. exists (c0 + 2*c). repeat split. (* - add *) - bitwise. + bitwise as m. destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0. rewrite <- !div2_bits, <- 2 lxor_spec. @@ -1320,7 +1323,7 @@ Proof. rewrite add_b2n_double_div2, <- IH1. apply add_carry_div2. (* - carry *) rewrite add_b2n_double_div2. - bitwise. + bitwise as m. destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. now rewrite add_b2n_double_bit0. rewrite <- !div2_bits, IH2. autorewrite with bitwise. @@ -1356,7 +1359,7 @@ Proof. symmetry in H. now apply lor_eq_0_l in H. intros EQ. rewrite EQ, lor_0_l in H. apply bits_inj_0. - induct n. trivial. + intro n; induct n. trivial. intros n IH. rewrite <- div2_bits, H. autorewrite with bitwise. @@ -1381,7 +1384,7 @@ Lemma ldiff_le : forall a b, ldiff a b == 0 -> a <= b. Proof. cut (forall n a b, a < 2^n -> ldiff a b == 0 -> a <= b). intros H a b. apply (H a), pow_gt_lin_r; order'. - induct n. + intro n; induct n. intros a b Ha _. rewrite pow_0_r, one_succ, lt_succ_r in Ha. assert (Ha' : a == 0) by (generalize (le_0_l a); order'). rewrite Ha'. apply le_0_l. @@ -1410,7 +1413,7 @@ Proof. rewrite sub_add. symmetry. rewrite add_nocarry_lxor. - bitwise. + bitwise as m. apply bits_inj_iff in H. specialize (H m). rewrite ldiff_spec, bits_0 in H. now destruct a.[m], b.[m]. @@ -1454,7 +1457,7 @@ Lemma add_nocarry_mod_lt_pow2 : forall a b n, land a b == 0 -> Proof. intros a b n H. apply add_nocarry_lt_pow2. - bitwise. + bitwise as m. destruct (le_gt_cases n m). now rewrite mod_pow2_bits_high. now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 9c50d5ca58..bb2f32935f 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -39,15 +39,15 @@ Qed. Theorem div_mod_unique : forall b q1 q2 r1 r2, r1<b -> r2<b -> b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2. -Proof. intros. apply div_mod_unique with b; auto'. Qed. +Proof. intros b q1 q2 r1 r2 ? ? ?. apply div_mod_unique with b; auto'. Qed. Theorem div_unique: forall a b q r, r<b -> a == b*q + r -> q == a/b. -Proof. intros; apply div_unique with r; auto'. Qed. +Proof. intros a b q r ? ?; apply div_unique with r; auto'. Qed. Theorem mod_unique: forall a b q r, r<b -> a == b*q + r -> r == a mod b. -Proof. intros. apply mod_unique with q; auto'. Qed. +Proof. intros a b q r ? ?. apply mod_unique with q; auto'. Qed. Theorem div_unique_exact: forall a b q, b~=0 -> a == b*q -> q == a/b. Proof. intros. apply div_unique_exact; auto'. Qed. diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v index a80ae8dc45..c1d8308e34 100644 --- a/theories/Numbers/Natural/Abstract/NGcd.v +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -53,7 +53,7 @@ Definition divide_gcd_iff' n m := divide_gcd_iff n m (le_0_l n). Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m. Proof. - intros. apply gcd_unique_alt'. + intros n m p. apply gcd_unique_alt'. intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial. apply divide_add_r; trivial. now apply divide_mul_r. apply divide_add_cancel_r with (p*n); trivial. @@ -98,11 +98,11 @@ Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m -> Bezout n m (gcd n m) /\ Bezout m n (gcd n m). Proof. intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. - pattern n. apply strong_right_induction with (z:=1); trivial. + pattern n. apply (fun H => strong_right_induction _ H 1); trivial. unfold Bezout. solve_proper. clear n Hn. intros n Hn IHn. intros m Hm. rewrite <- le_succ_l, <- one_succ in Hm. - pattern m. apply strong_right_induction with (z:=1); trivial. + pattern m. apply (fun H => strong_right_induction _ H 1); trivial. unfold Bezout. solve_proper. clear m Hm. intros m Hm IHm. destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. @@ -156,7 +156,7 @@ Qed. Theorem bezout_comm : forall a b g, b ~= 0 -> Bezout a b g -> Bezout b a g. Proof. - intros * Hbz (u & v & Huv). + intros a b g Hbz (u & v & Huv). destruct (eq_0_gt_0_cases a) as [Haz| Haz]. -rewrite Haz in Huv |-*. rewrite mul_0_r in Huv; symmetry in Huv. @@ -260,7 +260,7 @@ Qed. Lemma gcd_mul_mono_r : forall n m p, gcd (n*p) (m*p) == gcd n m * p. Proof. - intros. rewrite !(mul_comm _ p). apply gcd_mul_mono_l. + intros n m p. rewrite !(mul_comm _ p). apply gcd_mul_mono_l. Qed. Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p). diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 3a9cf34b25..b75b4521df 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -169,7 +169,7 @@ Qed. Lemma lcm_divide_iff : forall n m p, (lcm n m | p) <-> (n | p) /\ (m | p). Proof. - intros. split. split. + intros n m p. split. split. transitivity (lcm n m); trivial using divide_lcm_l. transitivity (lcm n m); trivial using divide_lcm_r. intros (H,H'). now apply lcm_least. diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v index ad6e2d65f0..3a41a2a560 100644 --- a/theories/Numbers/Natural/Abstract/NMaxMin.v +++ b/theories/Numbers/Natural/Abstract/NMaxMin.v @@ -42,95 +42,95 @@ Qed. (** Succ *) -Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m). +Lemma succ_max_distr n m : S (max n m) == max (S n) (S m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono. Qed. -Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m). +Lemma succ_min_distr n m : S (min n m) == min (S n) (S m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono. Qed. (** Add *) -Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m. +Lemma add_max_distr_l n m p : max (p + n) (p + m) == p + max n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l. Qed. -Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p. +Lemma add_max_distr_r n m p : max (n + p) (m + p) == max n m + p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r. Qed. -Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m. +Lemma add_min_distr_l n m p : min (p + n) (p + m) == p + min n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l. Qed. -Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p. +Lemma add_min_distr_r n m p : min (n + p) (m + p) == min n m + p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r. Qed. (** Mul *) -Lemma mul_max_distr_l : forall n m p, max (p * n) (p * m) == p * max n m. +Lemma mul_max_distr_l n m p : max (p * n) (p * m) == p * max n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_l. Qed. -Lemma mul_max_distr_r : forall n m p, max (n * p) (m * p) == max n m * p. +Lemma mul_max_distr_r n m p : max (n * p) (m * p) == max n m * p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_r. Qed. -Lemma mul_min_distr_l : forall n m p, min (p * n) (p * m) == p * min n m. +Lemma mul_min_distr_l n m p : min (p * n) (p * m) == p * min n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_l. Qed. -Lemma mul_min_distr_r : forall n m p, min (n * p) (m * p) == min n m * p. +Lemma mul_min_distr_r n m p : min (n * p) (m * p) == min n m * p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_r. Qed. (** Sub *) -Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m. +Lemma sub_max_distr_l n m p : max (p - n) (p - m) == p - min n m. Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite min_l by trivial. apply max_l. now apply sub_le_mono_l. rewrite min_r by trivial. apply max_r. now apply sub_le_mono_l. Qed. -Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p. +Lemma sub_max_distr_r n m p : max (n - p) (m - p) == max n m - p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r. Qed. -Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m. +Lemma sub_min_distr_l n m p : min (p - n) (p - m) == p - max n m. Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite max_r by trivial. apply min_r. now apply sub_le_mono_l. rewrite max_l by trivial. apply min_l. now apply sub_le_mono_l. Qed. -Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p. +Lemma sub_min_distr_r n m p : min (n - p) (m - p) == min n m - p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r. Qed. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 9a9a882239..ccdac104a3 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -46,19 +46,19 @@ Qed. Theorem lt_0_succ : forall n, 0 < S n. Proof. -induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r]. +intro n; induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r]. Qed. Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n. Proof. -cases n. +intro n; cases n. split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. Qed. Theorem eq_0_gt_0_cases : forall n, n == 0 \/ 0 < n. Proof. -cases n. +intro n; cases n. now left. intro; right; apply lt_0_succ. Qed. @@ -66,8 +66,8 @@ Qed. Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n. Proof. setoid_rewrite one_succ. -induct n. now left. -cases n. intros; right; now left. +intro n; induct n. now left. +intro n; cases n. intros; right; now left. intros n IH. destruct IH as [H | [H | H]]. false_hyp H neq_succ_0. right; right. rewrite H. apply lt_succ_diag_r. @@ -77,7 +77,7 @@ Qed. Theorem lt_1_r : forall n, n < 1 <-> n == 0. Proof. setoid_rewrite one_succ. -cases n. +intro n; cases n. split; intro; [reflexivity | apply lt_succ_diag_r]. intros n. rewrite <- succ_lt_mono. split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0]. @@ -86,7 +86,7 @@ Qed. Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1. Proof. setoid_rewrite one_succ. -cases n. +intro n; cases n. split; intro; [now left | apply le_succ_diag_r]. intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]]. @@ -101,7 +101,7 @@ Qed. Theorem lt_1_l' : forall n m p, n < m -> m < p -> 1 < p. Proof. -intros. apply lt_1_l with m; auto. +intros n m p H H0. apply lt_1_l with m; auto. apply le_lt_trans with n; auto. now apply le_0_l. Qed. @@ -117,7 +117,7 @@ Theorem le_ind_rel : (forall n m, n <= m -> R n m -> R (S n) (S m)) -> forall n m, n <= m -> R n m. Proof. -intros Base Step; induct n. +intros Base Step n; induct n. intros; apply Base. intros n IH m H. elim H using le_ind. solve_proper. @@ -130,7 +130,7 @@ Theorem lt_ind_rel : (forall n m, n < m -> R n m -> R (S n) (S m)) -> forall n m, n < m -> R n m. Proof. -intros Base Step; induct n. +intros Base Step n; induct n. intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. rewrite H; apply Base. intros n IH m H. elim H using lt_ind. @@ -151,14 +151,14 @@ Qed. Theorem le_pred_l : forall n, P n <= n. Proof. -cases n. +intro n; cases n. rewrite pred_0; now apply eq_le_incl. intros; rewrite pred_succ; apply le_succ_diag_r. Qed. Theorem lt_pred_l : forall n, n ~= 0 -> P n < n. Proof. -cases n. +intro n; cases n. intro H; exfalso; now apply H. intros; rewrite pred_succ; apply lt_succ_diag_r. Qed. @@ -176,7 +176,7 @@ Qed. Theorem lt_le_pred : forall n m, n < m -> n <= P m. (* Converse is false for n == m == 0 *) Proof. -intro n; cases m. +intros n m; cases m. intro H; false_hyp H nlt_0_r. intros m IH. rewrite pred_succ; now apply lt_succ_r. Qed. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index 58bc1499e1..4bb465c93c 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -16,19 +16,19 @@ Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N). Include NZParityProp N N NP. -Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n. +Lemma odd_pred n : n~=0 -> odd (P n) = even n. Proof. intros. rewrite <- (succ_pred n) at 2 by trivial. symmetry. apply even_succ. Qed. -Lemma even_pred : forall n, n~=0 -> even (P n) = odd n. +Lemma even_pred n : n~=0 -> even (P n) = odd n. Proof. intros. rewrite <- (succ_pred n) at 2 by trivial. symmetry. apply odd_succ. Qed. -Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m). +Lemma even_sub n m : m<=n -> even (n-m) = Bool.eqb (even n) (even m). Proof. intros. case_eq (even n); case_eq (even m); @@ -56,7 +56,7 @@ Proof. rewrite add_1_r in Hm,Hn. order. Qed. -Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m). +Lemma odd_sub n m : m<=n -> odd (n-m) = xorb (odd n) (odd m). Proof. intros. rewrite <- !negb_even. rewrite even_sub by trivial. now destruct (even n), (even m). diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v index 0b7720fd57..b49b6bf03c 100644 --- a/theories/Numbers/Natural/Abstract/NPow.v +++ b/theories/Numbers/Natural/Abstract/NPow.v @@ -55,7 +55,7 @@ Proof. wrap pow_mul_r. Qed. (** Power and nullity *) Lemma pow_eq_0 : forall a b, b~=0 -> a^b == 0 -> a == 0. -Proof. intros. apply (pow_eq_0 a b); trivial. auto'. Qed. +Proof. intros a b ? ?. apply (pow_eq_0 a b); trivial. auto'. Qed. Lemma pow_nonzero : forall a b, a~=0 -> a^b ~= 0. Proof. wrap pow_nonzero. Qed. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index e06604db53..b939352144 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -17,21 +17,21 @@ Include NMulOrderProp N. Theorem sub_0_l : forall n, 0 - n == 0. Proof. -induct n. +intro n; induct n. apply sub_0_r. intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0. Qed. Theorem sub_succ : forall n m, S n - S m == n - m. Proof. -intro n; induct m. +intros n m; induct m. rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ. intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r. Qed. Theorem sub_diag : forall n, n - n == 0. Proof. -induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. +intro n; induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. Qed. Theorem sub_gt : forall n m, n > m -> n - m ~= 0. @@ -96,7 +96,7 @@ Qed. Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p. Proof. -intros n m; induct p. +intros n m p; induct p. rewrite add_0_r; now rewrite sub_0_r. intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH. Qed. @@ -113,7 +113,7 @@ Qed. Theorem le_sub_l : forall n m, n - m <= n. Proof. -intro n; induct m. +intros n m; induct m. rewrite sub_0_r; now apply eq_le_incl. intros m IH. rewrite sub_succ_r. apply le_trans with (n - m); [apply le_pred_l | assumption]. @@ -121,7 +121,7 @@ Qed. Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m. Proof. -double_induct n m. +intros n m; double_induct n m. intro m; split; intro; [apply le_0_l | apply sub_0_l]. intro m; rewrite sub_0_r; split; intro H; [false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. @@ -130,7 +130,7 @@ Qed. Theorem sub_add_le : forall n m, n <= n - m + m. Proof. -intros. +intros n m. destruct (le_ge_cases n m) as [LE|GE]. rewrite <- sub_0_le in LE. rewrite LE; nzsimpl. now rewrite <- sub_0_le. @@ -216,12 +216,13 @@ Qed. Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p. Proof. - intros. rewrite le_sub_le_add_r. transitivity m. assumption. apply sub_add_le. + intros n m p. rewrite le_sub_le_add_r. + transitivity m. assumption. apply sub_add_le. Qed. Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n. Proof. - intros. rewrite le_sub_le_add_r. + intros n m p. rewrite le_sub_le_add_r. transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l]. Qed. @@ -264,14 +265,14 @@ Definition lt_alt n m := exists p, S p + n == m. Lemma le_equiv : forall n m, le_alt n m <-> n <= m. Proof. -split. +intros n m; split. intros (p,H). rewrite <- H, add_comm. apply le_add_r. intro H. exists (m-n). now apply sub_add. Qed. Lemma lt_equiv : forall n m, lt_alt n m <-> n < m. Proof. -split. +intros n m; split. intros (p,H). rewrite <- H, add_succ_l, lt_succ_r, add_comm. apply le_add_r. intro H. exists (m-S n). rewrite add_succ_l, <- add_succ_r. apply sub_add. now rewrite le_succ_l. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index e73060af0b..e97f2dc748 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -145,7 +145,7 @@ Qed. Lemma succ_inj p q : succ p = succ q -> p = q. Proof. revert q. - induction p; intros [q|q| ] H; simpl in H; destr_eq H; f_equal; auto. + induction p as [p|p|]; intros [q|q| ] H; simpl in H; destr_eq H; f_equal; auto. elim (succ_not_1 p); auto. elim (succ_not_1 q); auto. Qed. @@ -177,14 +177,14 @@ Qed. Theorem add_carry_spec p q : add_carry p q = succ (p + q). Proof. - revert q. induction p; destruct q; simpl; now f_equal. + revert q. induction p; intro q; destruct q; simpl; now f_equal. Qed. (** ** Commutativity *) Theorem add_comm p q : p + q = q + p. Proof. - revert q. induction p; destruct q; simpl; f_equal; trivial. + revert q. induction p; intro q; destruct q; simpl; f_equal; trivial. rewrite 2 add_carry_spec; now f_equal. Qed. @@ -193,7 +193,7 @@ Qed. Theorem add_succ_r p q : p + succ q = succ (p + q). Proof. revert q. - induction p; destruct q; simpl; f_equal; + induction p; intro q; destruct q; simpl; f_equal; auto using add_1_r; rewrite add_carry_spec; auto. Qed. @@ -247,13 +247,13 @@ Qed. Lemma add_carry_reg_r p q r : add_carry p r = add_carry q r -> p = q. Proof. - intros H. apply add_reg_r with (r:=r); now apply add_carry_add. + intros H. apply (add_reg_r _ _ r); now apply add_carry_add. Qed. Lemma add_carry_reg_l p q r : add_carry p q = add_carry p r -> q = r. Proof. - intros H; apply add_reg_r with (r:=p); + intros H; apply (add_reg_r _ _ p); rewrite (add_comm r), (add_comm q); now apply add_carry_add. Qed. @@ -288,7 +288,7 @@ Qed. Lemma add_xO_pred_double p q : pred_double (p + q) = p~0 + pred_double q. Proof. - revert q. induction p as [p IHp| p IHp| ]; destruct q; simpl; + revert q. induction p as [p IHp| p IHp| ]; intro q; destruct q; simpl; rewrite ?add_carry_spec, ?pred_double_succ, ?add_xI_pred_double; try reflexivity. rewrite IHp; auto. @@ -323,7 +323,7 @@ Theorem peano_rect_succ (P:positive->Type) (a:P 1) (f:forall p, P p -> P (succ p)) (p:positive) : peano_rect P a f (succ p) = f _ (peano_rect P a f p). Proof. - revert P a f. induction p; trivial. + revert P a f. induction p as [p IHp|p IHp|]; trivial. intros. simpl. now rewrite IHp. Qed. @@ -393,17 +393,17 @@ Qed. Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'. Proof. - intros. + intros p q q'. induction q as [ | p q IHq ]. apply eq_dep_eq_positive. - cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial. + cut (1=1). pattern 1 at 1 2 5, q'. destruct q' as [|p ?]. trivial. destruct p; intros; discriminate. trivial. apply eq_dep_eq_positive. - cut (succ p=succ p). pattern (succ p) at 1 2 5, q'. destruct q'. + cut (succ p=succ p). pattern (succ p) at 1 2 5, q'. destruct q' as [|? q']. intro. destruct p; discriminate. - intro. apply succ_inj in H. - generalize q'. rewrite H. intro. + intro H. apply succ_inj in H. + generalize q'. rewrite H. intro q'0. rewrite (IHq q'0). trivial. trivial. @@ -412,7 +412,7 @@ Qed. Lemma peano_equiv (P:positive->Type) (a:P 1) (f:forall p, P p -> P (succ p)) p : PeanoView_iter P a f p (peanoView p) = peano_rect P a f p. Proof. - revert P a f. induction p using peano_rect. + revert P a f. induction p as [|p IHp] using peano_rect. trivial. intros; simpl. rewrite peano_rect_succ. rewrite (PeanoViewUnique _ (peanoView (succ p)) (PeanoSucc _ (peanoView p))). @@ -575,11 +575,11 @@ Qed. (** ** Properties of [iter] *) -Lemma iter_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B), +Lemma iter_swap_gen A B (f:A->B)(g:A->A)(h:B->B) : (forall a, f (g a) = h (f a)) -> forall p a, f (iter g a p) = iter h (f a) p. Proof. - induction p; simpl; intros; now rewrite ?H, ?IHp. + intros H p; induction p as [p IHp|p IHp|]; simpl; intros; now rewrite ?H, ?IHp. Qed. Theorem iter_swap : @@ -593,7 +593,7 @@ Theorem iter_succ : forall p (A:Type) (f:A -> A) (x:A), iter f x (succ p) = f (iter f x p). Proof. - induction p as [p IHp|p IHp|]; intros; simpl; trivial. + intro p; induction p as [p IHp|p IHp|]; intros; simpl; trivial. now rewrite !IHp, iter_swap. Qed. @@ -608,18 +608,17 @@ Theorem iter_add : forall p q (A:Type) (f:A -> A) (x:A), iter f x (p+q) = iter f (iter f x q) p. Proof. - induction p using peano_ind; intros. + intro p; induction p as [|p IHp] using peano_ind; intros. now rewrite add_1_l, iter_succ. now rewrite add_succ_l, !iter_succ, IHp. Qed. -Theorem iter_ind : - forall (A:Type) (f:A -> A) (a:A) (P:positive -> A -> Prop), +Theorem iter_ind (A:Type) (f:A -> A) (a:A) (P:positive -> A -> Prop) : P 1 (f a) -> (forall p a', P p a' -> P (succ p) (f a')) -> forall p, P p (iter f a p). Proof. - induction p using peano_ind; trivial. + intros ? ? p; induction p as [|p IHp] using peano_ind; trivial. rewrite iter_succ; auto. Qed. @@ -628,7 +627,7 @@ Theorem iter_invariant : (forall x:A, Inv x -> Inv (f x)) -> forall x:A, Inv x -> Inv (iter f x p). Proof. - intros; apply iter_ind with (P := fun _ => Inv); auto. + intros; apply iter_ind; auto. Qed. (** ** Properties of power *) @@ -647,7 +646,7 @@ Qed. Lemma square_spec p : square p = p * p. Proof. - induction p. + induction p as [p IHp|p IHp|]. - rewrite square_xI. simpl. now rewrite IHp. - rewrite square_xO. simpl. now rewrite IHp. - trivial. @@ -658,13 +657,14 @@ Qed. Lemma sub_mask_succ_r p q : sub_mask p (succ q) = sub_mask_carry p q. Proof. - revert q. induction p; destruct q; simpl; f_equal; trivial; now destruct p. + revert q. induction p as [p ?|p ?|]; intro q; destruct q; + simpl; f_equal; trivial; now destruct p. Qed. Theorem sub_mask_carry_spec p q : sub_mask_carry p q = pred_mask (sub_mask p q). Proof. - revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl; + revert q. induction p as [p IHp|p IHp|]; intro q; destruct q as [q|q|]; simpl; try reflexivity; rewrite ?IHp; destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. @@ -676,16 +676,17 @@ Inductive SubMaskSpec (p q : positive) : mask -> Prop := Theorem sub_mask_spec p q : SubMaskSpec p q (sub_mask p q). Proof. - revert q. induction p; destruct q; simpl; try constructor; trivial. + revert q. induction p as [p IHp|p IHp|]; intro q; destruct q as [q|q|]; + simpl; try constructor; trivial. (* p~1 q~1 *) - destruct (IHp q); subst; try now constructor. + destruct (IHp q) as [|r|r]; subst; try now constructor. now apply SubIsNeg with r~0. (* p~1 q~0 *) - destruct (IHp q); subst; try now constructor. + destruct (IHp q) as [|r|r]; subst; try now constructor. apply SubIsNeg with (pred_double r). symmetry. apply add_xI_pred_double. (* p~0 q~1 *) rewrite sub_mask_carry_spec. - destruct (IHp q); subst; try constructor. + destruct (IHp q) as [|r|r]; subst; try constructor. now apply SubIsNeg with 1. destruct r; simpl; try constructor; simpl. now rewrite add_carry_spec, <- add_succ_r. @@ -693,7 +694,7 @@ Proof. now rewrite add_1_r. now apply SubIsNeg with r~1. (* p~0 q~0 *) - destruct (IHp q); subst; try now constructor. + destruct (IHp q) as [|r|r]; subst; try now constructor. now apply SubIsNeg with r~0. (* p~0 1 *) now rewrite add_1_l, succ_pred_double. @@ -707,7 +708,7 @@ Theorem sub_mask_nul_iff p q : sub_mask p q = IsNul <-> p = q. Proof. split. now case sub_mask_spec. - intros <-. induction p; simpl; now rewrite ?IHp. + intros <-. induction p as [p IHp|p IHp|]; simpl; now rewrite ?IHp. Qed. Theorem sub_mask_diag p : sub_mask p p = IsNul. @@ -752,7 +753,8 @@ Qed. Theorem eqb_eq p q : (p =? q) = true <-> p=q. Proof. - revert q. induction p; destruct q; simpl; rewrite ?IHp; split; congruence. + revert q. induction p as [p IHp|p IHp|]; intro q; destruct q; + simpl; rewrite ?IHp; split; congruence. Qed. Theorem ltb_lt p q : (p <? q) = true <-> p < q. @@ -786,7 +788,7 @@ Lemma compare_cont_spec p q c : Proof. unfold compare. revert q c. - induction p; destruct q; simpl; trivial. + induction p as [p IHp|p IHp|]; intro q; destruct q as [q|q|]; simpl; trivial. intros c. rewrite 2 IHp. now destruct (compare_cont Eq p q). intros c. @@ -1026,7 +1028,8 @@ Qed. Lemma compare_succ_succ p q : (succ p ?= succ q) = (p ?= q). Proof. revert q. - induction p; destruct q; simpl; simpl_compare; trivial; + induction p as [p|p|]; intro q; destruct q as [q|q|]; + simpl; simpl_compare; trivial; apply compare_succ_l || apply compare_succ_r || (now destruct p) || (now destruct q). Qed. @@ -1159,7 +1162,7 @@ Qed. Lemma add_compare_mono_l p q r : (p+q ?= p+r) = (q ?= r). Proof. - revert p q r. induction p using peano_ind; intros q r. + revert q r. induction p using peano_ind; intros q r. rewrite 2 add_1_l. apply compare_succ_succ. now rewrite 2 add_succ_l, compare_succ_succ. Qed. @@ -1214,7 +1217,7 @@ Qed. Lemma mul_compare_mono_l p q r : (p*q ?= p*r) = (q ?= r). Proof. - revert q r. induction p; simpl; trivial. + revert q r. induction p as [p IHp|p IHp|]; simpl; trivial. intros q r. specialize (IHp q r). destruct (compare_spec q r). subst. apply compare_refl. @@ -1265,7 +1268,7 @@ Qed. Lemma lt_add_r p q : p < p+q. Proof. - induction q using peano_ind. + induction q as [|q] using peano_ind. rewrite add_1_r. apply lt_succ_diag_r. apply lt_trans with (p+q); auto. apply add_lt_mono_l, lt_succ_diag_r. @@ -1476,10 +1479,11 @@ Qed. Lemma size_nat_monotone p q : p<q -> (size_nat p <= size_nat q)%nat. Proof. - assert (le0 : forall n, (0<=n)%nat) by (induction n; auto). + assert (le0 : forall n, (0<=n)%nat) by (intro n; induction n; auto). assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto). revert q. - induction p; destruct q; simpl; intros; auto; easy || apply leS; + induction p as [p IHp|p IHp|]; intro q; destruct q as [q|q|]; + simpl; intros H; auto; easy || apply leS; red in H; simpl_compare_in H. apply IHp. red. now destruct (p?=q). destruct (compare_spec p q); subst; now auto. @@ -1487,13 +1491,13 @@ Qed. Lemma size_gt p : p < 2^(size p). Proof. - induction p; simpl; try rewrite pow_succ_r; try easy. + induction p as [p IHp|p IHp|]; simpl; try rewrite pow_succ_r; try easy. apply le_succ_l in IHp. now apply le_succ_l. Qed. Lemma size_le p : 2^(size p) <= p~0. Proof. - induction p; simpl; try rewrite pow_succ_r; try easy. + induction p as [p IHp|p IHp|]; simpl; try rewrite pow_succ_r; try easy. apply mul_le_mono_l. apply le_lteq; left. rewrite xI_succ_xO. apply lt_succ_r, IHp. Qed. @@ -1612,7 +1616,7 @@ Lemma iter_op_succ : forall A (op:A->A->A), forall p a, iter_op op (succ p) a = op a (iter_op op p a). Proof. - induction p; simpl; intros; trivial. + intros A op H p; induction p as [p IHp|p IHp|]; simpl; intros; trivial. rewrite H. apply IHp. Qed. @@ -1620,7 +1624,7 @@ Qed. Lemma of_nat_succ (n:nat) : of_succ_nat n = of_nat (S n). Proof. - induction n. trivial. simpl. f_equal. now rewrite IHn. + induction n as [|n IHn]. trivial. simpl. f_equal. now rewrite IHn. Qed. Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n. @@ -1671,7 +1675,7 @@ Qed. Lemma sqrtrem_spec p : SqrtSpec (sqrtrem p) p. Proof. revert p. fix sqrtrem_spec 1. - destruct p; try destruct p; try (constructor; easy); + intro p; destruct p as [p|p|]; try destruct p; try (constructor; easy); apply sqrtrem_step_spec; auto. Qed. @@ -1688,7 +1692,7 @@ Proof. split. apply lt_le_incl, lt_add_r. rewrite <- add_1_l, mul_add_distr_r, !mul_add_distr_l, !mul_1_r, !mul_1_l. - rewrite add_assoc, (add_comm _ r). apply add_lt_mono_r. + rewrite add_assoc, (add_comm _ _). apply add_lt_mono_r. now rewrite <- add_assoc, add_diag, add_1_l, lt_succ_r. Qed. @@ -1710,7 +1714,7 @@ Lemma divide_xO_xI p q r : (p | q~0) -> (p | r~1) -> (p | q). Proof. intros (s,Hs) (t,Ht). destruct p. - destruct s; try easy. simpl in Hs. destr_eq Hs. now exists s. + destruct s as [s|s|]; try easy. simpl in Hs. destr_eq Hs. now exists s. rewrite mul_xO_r in Ht; discriminate. exists q; now rewrite mul_1_r. Qed. @@ -1738,9 +1742,9 @@ Qed. Lemma ggcdn_gcdn : forall n a b, fst (ggcdn n a b) = gcdn n a b. Proof. - induction n. + intro n; induction n as [|n IHn]. simpl; auto. - destruct a, b; simpl; auto; try case compare_spec; simpl; trivial; + intros a b; destruct a, b; simpl; auto; try case compare_spec; simpl; trivial; rewrite <- IHn; destruct ggcdn as (g,(u,v)); simpl; auto. Qed. @@ -1760,9 +1764,10 @@ Lemma ggcdn_correct_divisors : forall n a b, let '(g,(aa,bb)) := ggcdn n a b in a = g*aa /\ b = g*bb. Proof. - induction n. + intro n; induction n as [|n IHn]. simpl; auto. - destruct a, b; simpl; auto; try case compare_spec; try destr_pggcdn IHn. + intros a b; destruct a, b; + simpl; auto; try case compare_spec; try destr_pggcdn IHn. (* Eq *) intros ->. now rewrite mul_comm. (* Lt *) @@ -1809,9 +1814,9 @@ Qed. Lemma gcdn_greatest : forall n a b, (size_nat a + size_nat b <= n)%nat -> forall p, (p|a) -> (p|b) -> (p|gcdn n a b). Proof. - induction n. + intro n; induction n as [|n IHn]; intros a b. destruct a, b; simpl; inversion 1. - destruct a, b; simpl; try case compare_spec; simpl; auto. + destruct a as [a|a|], b as [b|b|]; simpl; try case compare_spec; simpl; auto. (* Lt *) intros LT LE p Hp1 Hp2. apply IHn; clear IHn; trivial. apply le_S_n in LE. eapply Le.le_trans; [|eapply LE]. @@ -1839,7 +1844,7 @@ Proof. apply divide_xO_xI with b; trivial. (* a~0 b~0 *) intros LE p Hp1 Hp2. - destruct p. + destruct p as [p|p|]. change (gcdn n a b)~0 with (2*(gcdn n a b)). apply divide_mul_r. apply IHn; clear IHn. @@ -1865,7 +1870,7 @@ Lemma ggcd_greatest : forall a b, let (aa,bb) := snd (ggcd a b) in forall p, (p|aa) -> (p|bb) -> p=1. Proof. - intros. generalize (gcd_greatest a b) (ggcd_correct_divisors a b). + intros a b **. generalize (gcd_greatest a b) (ggcd_correct_divisors a b). rewrite <- ggcd_gcd. destruct ggcd as (g,(aa,bb)); simpl. intros H (EQa,EQb) p Hp1 Hp2; subst. assert (H' : (g*p | g)). @@ -2126,7 +2131,7 @@ Qed. Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt. Proof. - destruct r; auto. + intro r; destruct r; auto. Qed. (** Incompatibilities : diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index abb33d462d..09c65f848f 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -32,14 +32,14 @@ Qed. Theorem inj_add p q : to_nat (p + q) = to_nat p + to_nat q. Proof. - revert q. induction p using peano_ind; intros q. + revert q. induction p as [|p IHp] using peano_ind; intros q. now rewrite add_1_l, inj_succ. now rewrite add_succ_l, !inj_succ, IHp. Qed. Theorem inj_mul p q : to_nat (p * q) = to_nat p * to_nat q. Proof. - revert q. induction p using peano_ind; simpl; intros; trivial. + revert q. induction p as [|p IHp] using peano_ind; simpl; intros; trivial. now rewrite mul_succ_l, inj_add, IHp, inj_succ. Qed. @@ -62,9 +62,9 @@ Qed. (** [Pos.to_nat] maps to the strictly positive subset of [nat] *) -Lemma is_succ : forall p, exists n, to_nat p = S n. +Lemma is_succ p : exists n, to_nat p = S n. Proof. - induction p using peano_ind. + induction p as [|p IHp] using peano_ind. now exists 0. destruct IHp as (n,Hn). exists (S n). now rewrite inj_succ, Hn. Qed. @@ -82,7 +82,7 @@ Qed. Theorem id p : of_nat (to_nat p) = p. Proof. - induction p using peano_ind. trivial. + induction p as [|p IHp] using peano_ind. trivial. rewrite inj_succ. rewrite <- IHp at 2. now destruct (is_succ p) as (n,->). Qed. @@ -149,7 +149,7 @@ Qed. Theorem inj_sub_max p q : to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q). Proof. - destruct (ltb_spec q p). + destruct (ltb_spec q p) as [H|H]. - (* q < p *) rewrite <- inj_sub by trivial. now destruct (is_succ (p - q)) as (m,->). @@ -192,11 +192,10 @@ Proof. - now apply Nat.max_l, Nat.lt_le_incl. Qed. -Theorem inj_iter : - forall p {A} (f:A->A) (x:A), +Theorem inj_iter p {A} (f:A->A) (x:A) : Pos.iter f x p = nat_rect _ x (fun _ => f) (to_nat p). Proof. - induction p using peano_ind. + induction p as [|p IHp] using peano_ind. - trivial. - intros. rewrite inj_succ, iter_succ. simpl. f_equal. apply IHp. @@ -443,7 +442,7 @@ Section ObsoletePmultNat. Lemma Pmult_nat_mult : forall p n, Pmult_nat p n = Pos.to_nat p * n. Proof. - induction p; intros n; unfold Pos.to_nat; simpl. + intro p; induction p as [p IHp|p IHp|]; intros n; unfold Pos.to_nat; simpl. f_equal. rewrite 2 IHp. rewrite <- Nat.mul_assoc. f_equal. simpl. now rewrite Nat.add_0_r. rewrite 2 IHp. rewrite <- Nat.mul_assoc. @@ -482,7 +481,7 @@ Qed. Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n. Proof. - intros. rewrite Pmult_nat_mult. + intros p n. rewrite Pmult_nat_mult. apply Nat.le_trans with (1*n). now rewrite Nat.mul_1_l. apply Nat.mul_le_mono_r. apply Pos2Nat.is_pos. Qed. diff --git a/theories/setoid_ring/BinList.v b/theories/setoid_ring/BinList.v index b6b8b45e1a..892909fd40 100644 --- a/theories/setoid_ring/BinList.v +++ b/theories/setoid_ring/BinList.v @@ -33,13 +33,13 @@ Section MakeBinList. Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l). Proof. - induction j;simpl;intros; now rewrite ?IHj. + intro j;induction j as [j IHj|j IHj|];simpl;intros; now rewrite ?IHj. Qed. Lemma jump_succ : forall j l, jump (Pos.succ j) l = jump 1 (jump j l). Proof. - induction j;simpl;intros. + intro j;induction j as [j IHj|j IHj|];simpl;intros. - rewrite !IHj; simpl; now rewrite !jump_tl. - now rewrite !jump_tl. - trivial. @@ -48,7 +48,7 @@ Section MakeBinList. Lemma jump_add : forall i j l, jump (i + j) l = jump i (jump j l). Proof. - induction i using Pos.peano_ind; intros. + intro i; induction i as [|i IHi] using Pos.peano_ind; intros. - now rewrite Pos.add_1_l, jump_succ. - now rewrite Pos.add_succ_l, !jump_succ, IHi. Qed. @@ -56,7 +56,7 @@ Section MakeBinList. Lemma jump_pred_double : forall i l, jump (Pos.pred_double i) (tl l) = jump i (jump i l). Proof. - induction i;intros;simpl. + intro i;induction i as [i IHi|i IHi|];intros;simpl. - now rewrite !jump_tl. - now rewrite IHi, <- 2 jump_tl, IHi. - trivial. @@ -64,7 +64,7 @@ Section MakeBinList. Lemma nth_jump : forall p l, nth p (tl l) = hd default (jump p l). Proof. - induction p;simpl;intros. + intro p;induction p as [p IHp|p IHp|];simpl;intros. - now rewrite <-jump_tl, IHp. - now rewrite <-jump_tl, IHp. - trivial. @@ -73,7 +73,7 @@ Section MakeBinList. Lemma nth_pred_double : forall p l, nth (Pos.pred_double p) (tl l) = nth p (jump p l). Proof. - induction p;simpl;intros. + intro p;induction p as [p IHp|p IHp|];simpl;intros. - now rewrite !jump_tl. - now rewrite jump_pred_double, <- !jump_tl, IHp. - trivial. diff --git a/theories/setoid_ring/Ring_theory.v b/theories/setoid_ring/Ring_theory.v index 230e789e21..32f21e2737 100644 --- a/theories/setoid_ring/Ring_theory.v +++ b/theories/setoid_ring/Ring_theory.v @@ -53,7 +53,7 @@ Section Power. Lemma pow_pos_swap x j : pow_pos x j * x == x * pow_pos x j. Proof. - induction j; simpl; rewrite <- ?mul_assoc. + induction j as [j IHj|j IHj|]; simpl; rewrite <- ?mul_assoc. - f_equiv. now do 2 (rewrite IHj, mul_assoc). - now do 2 (rewrite IHj, mul_assoc). - reflexivity. @@ -62,7 +62,7 @@ Section Power. Lemma pow_pos_succ x j : pow_pos x (Pos.succ j) == x * pow_pos x j. Proof. - induction j; simpl; try reflexivity. + induction j as [j IHj|j IHj|]; simpl; try reflexivity. rewrite IHj, <- mul_assoc; f_equiv. now rewrite mul_assoc, pow_pos_swap, mul_assoc. Qed. @@ -70,7 +70,7 @@ Section Power. Lemma pow_pos_add x i j : pow_pos x (i + j) == pow_pos x i * pow_pos x j. Proof. - induction i using Pos.peano_ind. + induction i as [|i IHi] using Pos.peano_ind. - now rewrite Pos.add_1_l, pow_pos_succ. - now rewrite Pos.add_succ_l, !pow_pos_succ, IHi, mul_assoc. Qed. |