diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Ints/num/QvMake.v | 8 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 29 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZTimesOrder.v | 17 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMinus.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 4 | ||||
| -rw-r--r-- | theories/QArith/Qpower.v | 12 |
9 files changed, 48 insertions, 49 deletions
diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v index e51291a041..c3db44bc6f 100644 --- a/theories/Ints/num/QvMake.v +++ b/theories/Ints/num/QvMake.v @@ -429,8 +429,8 @@ Module Qv. Theorem spec_sub x y: wf x -> wf y -> ([sub x y] == [x] - [y])%Q. intros x y Hx Hy; unfold sub; rewrite spec_add; auto. - apply wf_opp; auto. rewrite spec_opp; ring. + apply wf_opp; auto. Qed. Theorem spec_subc x y: wf x -> wf y -> @@ -450,8 +450,8 @@ Module Qv. Theorem spec_sub_norm x y: wf x -> wf y -> ([sub_norm x y] == [x] - [y])%Q. intros x y Hx Hy; unfold sub_norm; rewrite spec_add_norm; auto. - apply wf_opp; auto. rewrite spec_opp; ring. + apply wf_opp; auto. Qed. Theorem spec_sub_normc x y: wf x -> wf y -> @@ -945,10 +945,10 @@ Module Qv. Theorem spec_div x y: wf x -> wf y -> ([div x y] == [x] / [y])%Q. intros x y Hx Hy; unfold div; rewrite spec_mul; auto. - apply wf_inv; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. + apply wf_inv; auto. Qed. Theorem spec_divc x y: wf x -> wf y -> @@ -969,10 +969,10 @@ Module Qv. Theorem spec_div_norm x y: wf x -> wf y -> ([div_norm x y] == [x] / [y])%Q. intros x y Hx Hy; unfold div_norm; rewrite spec_mul_norm; auto. - apply wf_inv; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. + apply wf_inv; auto. Qed. Theorem spec_div_normc x y: wf x -> wf y -> diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 36a8458241..f0751f670a 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -802,7 +802,7 @@ Qed. Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q. Proof. intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ]; - simpl in |- *; auto; intro H; + simpl in |- *; auto; intro H ; [ rewrite (IHp q); trivial | absurd ((p ?= q) Gt = Eq); [ elim (Pcompare_not_Eq p q); auto | assumption ] diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index fc9115e20f..a40832507d 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -210,8 +210,9 @@ destruct n as [n m]. cut (forall p : N, A (p, 0)); [intro H1 |]. cut (forall p : N, A (0, p)); [intro H2 |]. destruct (plus_dichotomy n m) as [[p H] | [p H]]. -rewrite (A_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2. -rewrite (A_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1. +rewrite (A_wd (n, m) (0, p)) by (rewrite plus_0_l; now rewrite plus_comm). +apply H2. +rewrite (A_wd (n, m) (p, 0)) by now rewrite plus_0_r. apply H1. induct p. assumption. intros p IH. apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_1_l]. now apply <- AS. @@ -302,13 +303,13 @@ Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd. Proof. intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl. destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. -rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption. -rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)). +rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)) by now apply -> (NZle_wd n1 m1 H1 n2 m2 H2). stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring. unfold Zeq in H1. rewrite H1. ring. -rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption. -rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)). +rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)) by now apply -> (NZle_wd n2 m2 H2 n1 m1 H1). stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring. unfold Zeq in H2. rewrite H2. ring. @@ -318,13 +319,13 @@ Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd. Proof. intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl. destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. -rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption. -rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)). +rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)) by now apply -> (NZle_wd n1 m1 H1 n2 m2 H2). stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring. unfold Zeq in H2. rewrite H2. ring. -rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption. -rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)). +rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. +rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)) by now apply -> (NZle_wd n2 m2 H2 n1 m1 H1). stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring. unfold Zeq in H1. rewrite H1. ring. @@ -350,25 +351,25 @@ Qed. Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n. Proof. unfold Zmin, Zle, Zeq; simpl; intros n m H. -rewrite min_l. assumption. ring. +rewrite min_l by assumption. ring. Qed. Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m. Proof. unfold Zmin, Zle, Zeq; simpl; intros n m H. -rewrite min_r. assumption. ring. +rewrite min_r by assumption. ring. Qed. Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n. Proof. unfold Zmax, Zle, Zeq; simpl; intros n m H. -rewrite max_l. assumption. ring. +rewrite max_l by assumption. ring. Qed. Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m. Proof. unfold Zmax, Zle, Zeq; simpl; intros n m H. -rewrite max_r. assumption. ring. +rewrite max_r by assumption. ring. Qed. End NZOrdAxiomsMod. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index bc3600f9ce..133bbde4df 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -140,11 +140,12 @@ setoid_replace (n < n) with False using relation iff by now setoid_replace (S n <= n) with False using relation iff by (apply -> neg_false; apply NZnle_succ_diag_l). intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r. -rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m). +rewrite NZsucc_inj_wd. +rewrite (NZlt_eq_cases n m). rewrite or_cancel_r. +reflexivity. intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l. apply NZlt_neq. -reflexivity. Qed. Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m. diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 51d2172dec..b51e3d22b6 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -60,7 +60,7 @@ split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3. apply <- NZle_ngt in H3. le_elim H3. apply NZlt_asymm in H2. apply H2. now apply LR. rewrite H3 in H2; false_hyp H2 NZlt_irrefl. -rewrite (NZtimes_lt_pred p (S p)); [reflexivity |]. +rewrite (NZtimes_lt_pred p (S p)) by reflexivity. rewrite H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l. Qed. @@ -109,9 +109,9 @@ assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |]. rewrite H1 in H4; false_hyp H4 NZlt_irrefl. false_hyp H2 H. apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |]. +assert (H4 : p * n < p * m) by (now apply -> NZtimes_lt_mono_pos_l). rewrite H1 in H4; false_hyp H4 NZlt_irrefl. -assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |]. +assert (H4 : p * m < p * n) by (now apply -> NZtimes_lt_mono_pos_l). rewrite H1 in H4; false_hyp H4 NZlt_irrefl. now rewrite H1. Qed. @@ -135,9 +135,9 @@ Qed. Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m). Proof. intros n m p H; do 2 rewrite NZlt_eq_cases. -rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |]. -now rewrite -> (NZtimes_cancel_l n m p); -[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. +rewrite (NZtimes_lt_mono_pos_l p n m) by assumption. +now rewrite -> (NZtimes_cancel_l n m p) by +(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). Qed. Theorem NZtimes_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p). @@ -149,9 +149,8 @@ Qed. Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n). Proof. intros n m p H; do 2 rewrite NZlt_eq_cases. -rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |]. -rewrite -> (NZtimes_cancel_l m n p); -[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |]. +rewrite (NZtimes_lt_mono_neg_l p n m); [| assumption]. +rewrite -> (NZtimes_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl). now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro). Qed. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 10c341cbfa..4df46e20eb 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ : forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n). Proof. unfold natural_isomorphism. -intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq); -[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |]. +intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ; +[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd]. Qed. Theorem hom_nat_iso : homomorphism natural_isomorphism. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index faf4759bdb..5e1d5d8c3c 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -63,8 +63,8 @@ Proof. intros n m p; induct p. intro; now do 2 rewrite minus_0_r. intros p IH H. do 2 rewrite minus_succ_r. -rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |]. -rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l. +rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). +rewrite plus_pred_r by (apply minus_gt; now apply -> le_succ_l). reflexivity. Qed. @@ -76,13 +76,13 @@ Qed. Theorem plus_minus : forall n m : N, (n + m) - m == n. Proof. -intros n m. rewrite <- plus_minus_assoc. apply le_refl. +intros n m. rewrite <- plus_minus_assoc by (apply le_refl). rewrite minus_diag; now rewrite plus_0_r. Qed. Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m. Proof. -intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |]. +intros n m H. rewrite plus_comm. rewrite plus_minus_assoc by assumption. rewrite plus_comm. apply plus_minus. Qed. @@ -121,7 +121,7 @@ Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m. Proof. intros n m p H. rewrite (plus_comm n m). -rewrite <- plus_minus_assoc; [assumption |]. +rewrite <- plus_minus_assoc by assumption. now rewrite (plus_comm m (n - p)). Qed. @@ -151,8 +151,8 @@ Proof. intros n m; cases m. now rewrite pred_0, times_0_r, minus_0_l. intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc. -now apply eq_le_incl. now rewrite minus_diag, plus_0_r. +now apply eq_le_incl. Qed. Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. @@ -160,9 +160,9 @@ Proof. intros n m p; induct n. now rewrite minus_0_l, times_0_l, minus_0_l. intros n IH. destruct (le_gt_cases m n) as [H | H]. -rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l. +rewrite minus_succ_l by assumption. do 2 rewrite times_succ_l. rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p). -rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |]. +rewrite <- (plus_minus_assoc p (n * p) (m * p)) by now apply times_le_mono_r. now apply <- plus_cancel_l. assert (H1 : S n <= m); [now apply <- le_succ_l |]. setoid_replace (S n - m) with 0 by now apply <- minus_0_le. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 7b4645be35..1e53d80637 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -506,7 +506,7 @@ Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m). Proof. intros n m H1; split; intro H2. assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n. -now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2; +now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ; [apply <- succ_lt_mono | | |]. assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n). apply lt_le_trans with (P m). assumption. apply le_pred_l. @@ -515,7 +515,7 @@ Qed. Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m. Proof. -intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ. +intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ. Qed. Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 78034802fa..8672592d90 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -121,8 +121,8 @@ destruct (Qeq_dec a 0). rewrite q. repeat rewrite Qpower_positive_0. reflexivity. -rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)). - apply Qpower_not_0_positive; assumption. +rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by + (apply Qpower_not_0_positive; assumption). apply Qdiv_comp;[|reflexivity]. rewrite Qmult_comm. rewrite <- Qpower_plus_positive. @@ -150,8 +150,7 @@ Proof. intros a n m H. destruct (Qeq_dec a 0)as [X|X]. rewrite X. -rewrite Qpower_0. -assumption. +rewrite Qpower_0 by assumption. destruct n; destruct m; try (elim H; reflexivity); simpl; repeat rewrite Qpower_positive_0; ring_simplify; reflexivity. @@ -191,9 +190,8 @@ induction n using Pind. rewrite Zpos_succ_morphism. unfold Zsucc. rewrite Zpower_exp; auto with *; try discriminate. -rewrite Qpower_plus'; try discriminate. -rewrite <- IHn. - discriminate. +rewrite Qpower_plus' by discriminate. +rewrite <- IHn by discriminate. replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring. ring_simplify. reflexivity. |