diff options
32 files changed, 275 insertions, 376 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 8f7bab072..b2994e632 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -81,6 +81,21 @@ Export ProperNotations. Open Local Scope signature_scope. +(** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f] + by repeated introductions and setoid rewrites. It should work + fine when [f] is a combination of already known morphisms and + quantifiers. *) + +Ltac solve_respectful t := + match goal with + | |- respectful _ _ _ _ => + let H := fresh "H" in + intros ? ? H; solve_respectful ltac:(setoid_rewrite H; t) + | _ => t; reflexivity + end. + +Ltac solve_proper := unfold Proper; solve_respectful ltac:(idtac). + (** Dependent pointwise lifting of a relation on the range. *) Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) := diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index d4ce9aaa9..256bcc377 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -107,3 +107,33 @@ Program Instance all_inverse_impl_morphism {A : Type} : unfold pointwise_relation, all in *. intuition ; specialize (H x0) ; intuition. Qed. + +(** Equivalent points are simultaneously accessible or not *) + +Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop) + `(Equivalence _ E) `(Proper _ (E==>E==>iff) R) : + Proper (E==>iff) (Acc R). +Proof. + apply proper_sym_impl_iff; auto with *. + intros x y EQ WF. apply Acc_intro; intros z Hz. + rewrite <- EQ in Hz. now apply Acc_inv with x. +Qed. + +(** Equivalent relations have the same accessible points *) + +Instance Acc_rel_morphism {A:Type} : + Proper (@relation_equivalence A ==> Logic.eq ==> iff) (@Acc A). +Proof. + apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry. + intros R R' EQ a a' Ha WF. subst a'. + induction WF as [x _ WF']. constructor. + intros y Ryx. now apply WF', EQ. +Qed. + +(** Equivalent relations are simultaneously well-founded or not *) + +Instance well_founded_morphism {A : Type} : + Proper (@relation_equivalence A ==> iff) (@well_founded A). +Proof. + unfold well_founded. solve_proper. +Qed. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index fd192dce6..c52cbe105 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -134,7 +134,7 @@ Qed. Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1). Proof. intros n H1 H2 H3. -unfold B in *. apply -> AS in H3. +unfold B in *. apply AS in H3. setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption. zify. rewrite 2 ZnZ.of_Z_correct; auto with zarith. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 44cd08e67..641375a5c 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -347,7 +347,7 @@ Qed. Lemma div_pow2_bits : forall a n m, 0<=n -> 0<=m -> (a/2^n).[m] = a.[m+n]. Proof. intros a n m Hn. revert a m. apply le_ind with (4:=Hn). - solve_predicate_wd. + solve_proper. intros a m Hm. now nzsimpl. clear n Hn. intros n Hn IH a m Hm. nzsimpl; trivial. rewrite <- div_div by order_pos. @@ -360,7 +360,7 @@ Proof. destruct (le_gt_cases 0 n) as [Hn|Hn]. now rewrite <- div2_bits, mul_comm, div_mul by order'. rewrite (testbit_neg_r a n Hn). - apply le_succ_l, le_lteq in Hn. destruct Hn as [Hn|Hn]. + apply le_succ_l in Hn. le_elim Hn. now rewrite testbit_neg_r. now rewrite Hn, bit0_odd, odd_mul, odd_2. Qed. @@ -373,7 +373,7 @@ Qed. Lemma mul_pow2_bits_add : forall a n m, 0<=n -> (a*2^n).[n+m] = a.[m]. Proof. intros a n m Hn. revert a m. apply le_ind with (4:=Hn). - solve_predicate_wd. + solve_proper. intros a m. now nzsimpl. clear n Hn. intros n Hn IH a m. nzsimpl; trivial. rewrite mul_assoc, (mul_comm _ 2), <- mul_assoc. @@ -403,11 +403,11 @@ Lemma mod_pow2_bits_high : forall a n m, 0<=n<=m -> Proof. intros a n m (Hn,H). destruct (mod_pos_bound a (2^n)) as [LE LT]. order_pos. - apply le_lteq in LE; destruct LE as [LT'|EQ]. + le_elim LE. apply bits_above_log2; try order. apply lt_le_trans with n; trivial. apply log2_lt_pow2; trivial. - now rewrite <-EQ, bits_0. + now rewrite <- LE, bits_0. Qed. Lemma mod_pow2_bits_low : forall a n m, m<n -> @@ -463,7 +463,7 @@ Proof. assert (AUX : forall n, 0<=n -> forall a b, 0<=a<2^n -> testbit a === testbit b -> a == b). intros n Hn. apply le_ind with (4:=Hn). - solve_predicate_wd. + solve_proper. intros a b Ha H. rewrite pow_0_r, one_succ, lt_succ_r in Ha. assert (Ha' : a == 0) by (destruct Ha; order). rewrite Ha' in *. @@ -553,10 +553,10 @@ Proof. exists 0. intros m Hm. now rewrite bits_0, H0. clear k LE. intros k LE IH f Hf Hk. destruct (IH (fun m => f (S m))) as (n, Hn). - solve_predicate_wd. + solve_proper. intros m Hm. apply Hk. now rewrite <- succ_le_mono. exists (f 0 + 2*n). intros m Hm. - apply le_lteq in Hm. destruct Hm as [Hm|Hm]. + le_elim Hm. rewrite <- (succ_pred m), Hn, <- div2_bits. rewrite mul_comm, div_add, b2z_div2, add_0_l; trivial. order'. now rewrite <- lt_succ_r, succ_pred. @@ -743,10 +743,8 @@ Qed. Lemma shiftr_eq_0 : forall a n, 0<=a -> log2 a < n -> a >> n == 0. Proof. - intros a n Ha H. - apply shiftr_eq_0_iff. - apply le_lteq in Ha. destruct Ha as [Ha|Ha]. - right. now split. now left. + intros a n Ha H. apply shiftr_eq_0_iff. + le_elim Ha. right. now split. now left. Qed. (** Properties of [div2]. *) @@ -1304,7 +1302,7 @@ Qed. Lemma ones_spec_high : forall n m, 0<=n<=m -> (ones n).[m] = false. Proof. - intros n m (Hn,H). apply le_lteq in Hn. destruct Hn as [Hn|Hn]. + intros n m (Hn,H). le_elim Hn. apply bits_above_log2; rewrite ones_equiv. rewrite <-lt_succ_r, succ_pred; order_pos. rewrite log2_pred_pow2; trivial. now rewrite <-le_succ_l, succ_pred. @@ -1576,7 +1574,7 @@ Lemma log2_lor : forall a b, 0<=a -> 0<=b -> Proof. assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lor a b) == log2 b). intros a b Ha H. - apply le_lteq in Ha; destruct Ha as [Ha|Ha]; [|now rewrite <- Ha, lor_0_l]. + le_elim Ha; [|now rewrite <- Ha, lor_0_l]. apply log2_bits_unique. now rewrite lor_spec, bit_log2, orb_true_r by order. intros m Hm. assert (H' := log2_le_mono _ _ H). @@ -1594,12 +1592,12 @@ Lemma log2_land : forall a b, 0<=a -> 0<=b -> Proof. assert (AUX : forall a b, 0<=a -> a<=b -> log2 (land a b) <= log2 a). intros a b Ha Hb. - apply le_ngt. intros H'. - assert (LE : 0 <= land a b) by (apply land_nonneg; now left). - apply le_lteq in LE. destruct LE as [LT|EQ]. - generalize (bit_log2 (land a b) LT). + apply le_ngt. intros LT. + assert (H : 0 <= land a b) by (apply land_nonneg; now left). + le_elim H. + generalize (bit_log2 (land a b) H). now rewrite land_spec, bits_above_log2. - rewrite <- EQ in H'. apply log2_lt_cancel in H'; order. + rewrite <- H in LT. apply log2_lt_cancel in LT; order. (* main *) intros a b Ha Hb. destruct (le_ge_cases a b) as [H|H]. @@ -1612,13 +1610,13 @@ Lemma log2_lxor : forall a b, 0<=a -> 0<=b -> Proof. assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lxor a b) <= log2 b). intros a b Ha Hb. - apply le_ngt. intros H'. - assert (LE : 0 <= lxor a b) by (apply lxor_nonneg; split; order). - apply le_lteq in LE. destruct LE as [LT|EQ]. - generalize (bit_log2 (lxor a b) LT). + apply le_ngt. intros LT. + assert (H : 0 <= lxor a b) by (apply lxor_nonneg; split; order). + le_elim H. + generalize (bit_log2 (lxor a b) H). rewrite lxor_spec, 2 bits_above_log2; try order. discriminate. apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono. - rewrite <- EQ in H'. apply log2_lt_cancel in H'; order. + rewrite <- H in LT. apply log2_lt_cancel in LT; order. (* main *) intros a b Ha Hb. destruct (le_ge_cases a b) as [H|H]. @@ -1679,13 +1677,12 @@ Lemma add_carry_bits_aux : forall n, 0<=n -> a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0. Proof. intros n Hn. apply le_ind with (4:=Hn). - solve_predicate_wd. + solve_proper. (* base *) intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r, <- !one_succ. intros (Ha1,Ha2) (Hb1,Hb2). - apply le_lteq in Ha1; apply le_lteq in Hb1. - rewrite <- le_succ_l, succ_m1 in Ha1, Hb1. - destruct Ha1 as [Ha1|Ha1]; destruct Hb1 as [Hb1|Hb1]. + le_elim Ha1; rewrite <- ?le_succ_l, ?succ_m1 in Ha1; + le_elim Hb1; rewrite <- ?le_succ_l, ?succ_m1 in Hb1. (* base, a = 0, b = 0 *) exists c0. rewrite (le_antisymm _ _ Ha2 Ha1), (le_antisymm _ _ Hb2 Hb1). @@ -1727,7 +1724,7 @@ Proof. exists (c0 + 2*c). repeat split. (* step, add *) bitwise. - apply le_lteq in Hm. destruct Hm as [Hm|Hm]. + le_elim Hm. rewrite <- (succ_pred m), lt_succ_r in Hm. rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial. apply testbit_wd; try easy. @@ -1737,7 +1734,7 @@ Proof. (* step, carry *) rewrite add_b2z_double_div2. bitwise. - apply le_lteq in Hm. destruct Hm as [Hm|Hm]. + le_elim Hm. rewrite <- (succ_pred m), lt_succ_r in Hm. rewrite <- (succ_pred m), <- !div2_bits, IH2 by trivial. autorewrite with bitwise. now rewrite add_b2z_double_div2. @@ -1801,7 +1798,7 @@ Proof. intros EQ. rewrite EQ, lor_0_l in H. apply bits_inj'. intros n Hn. rewrite bits_0. apply le_ind with (4:=Hn). - solve_predicate_wd. + solve_proper. trivial. clear n Hn. intros n Hn IH. rewrite <- div2_bits, H; trivial. @@ -1828,7 +1825,7 @@ Proof. assert (AUX : forall n, 0<=n -> forall a b, 0 <= a < 2^n -> 0<=b -> ldiff a b == 0 -> a <= b). intros n Hn. apply le_ind with (4:=Hn); clear n Hn. - solve_predicate_wd. + solve_proper. intros a b Ha Hb _. rewrite pow_0_r, one_succ, lt_succ_r in Ha. setoid_replace a with 0 by (destruct Ha; order'); trivial. intros n Hn IH a b (Ha,Ha') Hb H. diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index 77a7c7341..87a95e9d7 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -163,12 +163,12 @@ Proof. assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)). intros n Hn; pattern n. apply strong_right_induction with (z:=0); trivial. - unfold Bezout. solve_predicate_wd. + unfold Bezout. solve_proper. clear n Hn. intros n Hn IHn. apply le_lteq in Hn; destruct Hn as [Hn|Hn]. intros m Hm; pattern m. apply strong_right_induction with (z:=0); trivial. - unfold Bezout. solve_predicate_wd. + unfold Bezout. solve_proper. clear m Hm. intros m Hm IHm. destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. (* n < m *) diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index bbf7d893a..f381953fb 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -313,8 +313,8 @@ Lemma lcm_unique_alt : forall n m p, 0<=p -> Proof. intros n m p Hp H. apply lcm_unique; trivial. - apply -> H. apply divide_refl. - apply -> H. apply divide_refl. + apply H, divide_refl. + apply H, divide_refl. intros. apply H. now split. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 5431b4a10..3a8e1f389 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -68,12 +68,12 @@ Qed. Theorem lt_lt_pred : forall n m, n < m -> P n < m. Proof. -intros; apply <- lt_pred_le; now apply lt_le_incl. +intros; apply lt_pred_le; now apply lt_le_incl. Qed. Theorem le_le_pred : forall n m, n <= m -> P n <= m. Proof. -intros; apply lt_le_incl; now apply <- lt_pred_le. +intros; apply lt_le_incl; now apply lt_pred_le. Qed. Theorem lt_pred_lt : forall n m, n < P m -> n < m. @@ -83,7 +83,7 @@ Qed. Theorem le_pred_lt : forall n m, n <= P m -> n <= m. Proof. -intros; apply lt_le_incl; now apply <- lt_le_pred. +intros; apply lt_le_incl; now apply lt_le_pred. Qed. Theorem pred_lt_mono : forall n m, n < m <-> P n < P m. @@ -123,9 +123,9 @@ Qed. Theorem lt_m1_r : forall n m, n < m -> m < 0 -> n < -1. Proof. -intros n m H1 H2. apply -> lt_le_pred in H2. +intros n m H1 H2. apply lt_le_pred in H2. setoid_replace (P 0) with (-1) in H2. now apply lt_le_trans with m. -apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0. +apply eq_opp_r. now rewrite one_succ, opp_pred, opp_0. Qed. End ZOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 68eca3305..618722aa8 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -39,7 +39,7 @@ Qed. Theorem mul_opp_l : forall n m, (- n) * m == - (n * m). Proof. -intros n m. apply -> add_move_0_r. +intros n m. apply add_move_0_r. now rewrite <- mul_add_distr_r, add_opp_diag_l, mul_0_l. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 4c0a9a2ca..6d2fa41fc 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -94,7 +94,7 @@ Notation le_0_square := square_nonneg (only parsing). Theorem nlt_square_0 : forall n, ~ n * n < 0. Proof. -intros n H. apply -> lt_nge in H. apply H. apply square_nonneg. +intros n H. apply lt_nge in H. apply H. apply square_nonneg. Qed. Theorem square_lt_mono_nonpos : forall n m, n <= 0 -> m < n -> n * n < m * m. @@ -109,42 +109,38 @@ Qed. Theorem square_lt_simpl_nonpos : forall n m, m <= 0 -> n * n < m * m -> m < n. Proof. -intros n m H1 H2. destruct (le_gt_cases n 0). -destruct (lt_ge_cases m n). -assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonpos. -apply -> le_ngt in F. false_hyp H2 F. -now apply le_lt_trans with 0. +intros n m H1 H2. destruct (le_gt_cases n 0); [|order]. +destruct (lt_ge_cases m n) as [LE|GT]; trivial. +apply square_le_mono_nonpos in GT; order. Qed. Theorem square_le_simpl_nonpos : forall n m, m <= 0 -> n * n <= m * m -> m <= n. Proof. -intros n m H1 H2. destruct (le_gt_cases n 0). -destruct (le_gt_cases m n). -assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonpos. -apply -> lt_nge in F. false_hyp H2 F. -apply lt_le_incl; now apply le_lt_trans with 0. +intros n m H1 H2. destruct (le_gt_cases n 0); [|order]. +destruct (le_gt_cases m n) as [LE|GT]; trivial. +apply square_lt_mono_nonpos in GT; order. Qed. Theorem lt_1_mul_neg : forall n m, n < -1 -> m < 0 -> 1 < n * m. Proof. -intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1. -apply <- opp_pos_neg in H2. rewrite mul_opp_l, mul_1_l in H1. +intros n m H1 H2. apply (mul_lt_mono_neg_r m) in H1. +apply opp_pos_neg in H2. rewrite mul_opp_l, mul_1_l in H1. now apply lt_1_l with (- m). assumption. Qed. Theorem lt_mul_m1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1. Proof. -intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1. +intros n m H1 H2. apply (mul_lt_mono_neg_r m) in H1. rewrite mul_1_l in H1. now apply lt_m1_r with m. assumption. Qed. Theorem lt_mul_m1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1. Proof. -intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1. +intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1. rewrite mul_opp_l, mul_1_l in H1. -apply <- opp_neg_pos in H2. now apply lt_m1_r with (- m). +apply opp_neg_pos in H2. now apply lt_m1_r with (- m). assumption. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 682c680cc..53d84dce1 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -22,7 +22,7 @@ Module Type ZPowProp Lemma even_pow : forall a b, 0<b -> even (a^b) = even a. Proof. - intros a b Hb. apply lt_ind with (4:=Hb). solve_predicate_wd. + intros a b Hb. apply lt_ind with (4:=Hb). solve_proper. now nzsimpl. clear b Hb. intros b Hb IH. nzsimpl; [|order]. rewrite even_mul, IH. now destruct (even a). diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 8ed42ed8d..cad5152d7 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -23,7 +23,7 @@ Proof. intros A A_wd A0 AS n; apply Zind; clear n. assumption. intros; rewrite <- Zsucc_succ'. now apply -> AS. -intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS. +intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply AS. Qed. (** * Implementation of [ZAxiomsMiniSig] by [BinInt.Z] *) diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index ab555ca32..2b568dddc 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,7 +13,7 @@ Require Export Ring. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Open Local Scope pair_scope. +Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. @@ -173,8 +173,8 @@ rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm). apply H2. rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1. induct p. assumption. intros p IH. -apply -> (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. -rewrite one_succ in IH. now apply <- AS. +apply (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. +rewrite one_succ in IH. now apply AS. induct p. assumption. intros p IH. replace 0 with (snd (p, 0)); [| reflexivity]. replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 3aa6f41d3..fdec8ceb7 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -28,7 +28,7 @@ Theorem add_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q. Proof. intros n m p q H1 H2. apply lt_trans with (m + p); -[now apply -> add_lt_mono_r | now apply -> add_lt_mono_l]. +[now apply add_lt_mono_r | now apply add_lt_mono_l]. Qed. Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m. @@ -46,21 +46,21 @@ Theorem add_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q. Proof. intros n m p q H1 H2. apply le_trans with (m + p); -[now apply -> add_le_mono_r | now apply -> add_le_mono_l]. +[now apply add_le_mono_r | now apply add_le_mono_l]. Qed. Theorem add_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q. Proof. intros n m p q H1 H2. apply lt_le_trans with (m + p); -[now apply -> add_lt_mono_r | now apply -> add_le_mono_l]. +[now apply add_lt_mono_r | now apply add_le_mono_l]. Qed. Theorem add_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q. Proof. intros n m p q H1 H2. apply le_lt_trans with (m + p); -[now apply -> add_le_mono_r | now apply -> add_lt_mono_l]. +[now apply add_le_mono_r | now apply add_lt_mono_l]. Qed. Theorem add_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n + m. @@ -154,7 +154,7 @@ Qed. Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p. Proof. - intros n m H. apply le_ind with (4:=H). solve_predicate_wd. + intros n m H. apply le_ind with (4:=H). solve_proper. exists 0; nzsimpl; split; order. clear m H. intros m H (p & EQ & LE). exists (S p). split. nzsimpl. now apply succ_wd. now apply le_le_succ_r. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index a86fec3fd..7c7f43de0 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -48,7 +48,7 @@ Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2. Proof. intros; split. apply succ_inj. -apply succ_wd. +intros. now apply succ_wd. Qed. Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m. @@ -61,7 +61,7 @@ left-inverse to the successor at this point *) Section CentralInduction. -Variable A : predicate t. +Variable A : t -> Prop. Hypothesis A_wd : Proper (eq==>iff) A. Theorem central_induction : @@ -70,7 +70,7 @@ Theorem central_induction : forall n, A n. Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. -solve_predicate_wd. +solve_proper. intro; now apply bi_induction. intro; pose proof (Step n); tauto. Qed. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index 9c022646b..6788cd4e8 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder. (** Interface of a gcd function, then its specification on naturals *) Module Type Gcd (Import A : Typ). - Parameters Inline gcd : t -> t -> t. + Parameter Inline gcd : t -> t -> t. End Gcd. Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A). @@ -71,12 +71,12 @@ Lemma eq_mul_1_nonneg : forall n m, 0<=n -> n*m == 1 -> n==1 /\ m==1. Proof. intros n m Hn H. - apply le_lteq in Hn. destruct Hn as [Hn|Hn]. + le_elim Hn. destruct (lt_ge_cases m 0) as [Hm|Hm]. generalize (mul_pos_neg n m Hn Hm). order'. - apply le_lteq in Hm. destruct Hm as [Hm|Hm]. + le_elim Hm. apply le_succ_l in Hn. rewrite <- one_succ in Hn. - apply le_lteq in Hn. destruct Hn as [Hn|Hn]. + le_elim Hn. generalize (lt_1_mul_pos n m Hn Hm). order. rewrite <- Hn, mul_1_l in H. now split. rewrite <- Hm, mul_0_r in H. order'. @@ -108,7 +108,7 @@ Lemma divide_antisym_nonneg : forall n m, 0<=n -> 0<=m -> (n | m) -> (m | n) -> n == m. Proof. intros n m Hn Hm (q,Hq) (r,Hr). - apply le_lteq in Hn. destruct Hn as [Hn|Hn]. + le_elim Hn. destruct (lt_ge_cases q 0) as [Hq'|Hq']. generalize (mul_pos_neg n q Hn Hq'). order. rewrite <- Hq, <- mul_assoc in Hr. @@ -175,7 +175,7 @@ Proof. rewrite <- Hq. destruct (lt_ge_cases q 0) as [Hq'|Hq']. generalize (mul_pos_neg n q Hn Hq'). order. - apply le_lteq in Hq'. destruct Hq' as [Hq'|Hq']. + le_elim Hq'. rewrite <- (mul_1_r n) at 1. apply mul_le_mono_pos_l; trivial. now rewrite one_succ, le_succ_l. rewrite <- Hq', mul_0_r in Hq. order. @@ -219,8 +219,8 @@ Lemma gcd_unique_alt : forall n m p, 0<=p -> Proof. intros n m p Hp H. apply gcd_unique; trivial. - apply -> H. apply divide_refl. - apply -> H. apply divide_refl. + apply H. apply divide_refl. + apply H. apply divide_refl. intros. apply H. now split. Qed. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 6e1c2b3a1..a5aa6d8ac 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder NZPow. (** Interface of a log2 function, then its specification on naturals *) Module Type Log2 (Import A : Typ). - Parameters Inline log2 : t -> t. + Parameter Inline log2 : t -> t. End Log2. Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A). @@ -155,8 +155,7 @@ Lemma log2_pos : forall a, 1<a -> 0 < log2 a. Proof. intros a Ha. assert (Ha' : 0 < a) by order'. - assert (H := log2_nonneg a). apply le_lteq in H. - destruct H; trivial. + assert (H := log2_nonneg a). le_elim H; trivial. generalize (log2_spec a Ha'). rewrite <- H in *. nzsimpl; try order. intros (_,H'). rewrite two_succ in H'. apply lt_succ_r in H'; order. Qed. @@ -168,7 +167,7 @@ Proof. intros a. split; intros H. destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. generalize (log2_pos a Ha); order. - apply le_lteq in H; destruct H. + le_elim H. apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ. rewrite H. apply log2_1. Qed. @@ -246,7 +245,7 @@ Qed. Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a. Proof. intros a Ha. - apply le_lteq in Ha; destruct Ha as [Ha|Ha]. + le_elim Ha. now apply lt_le_incl, log2_lt_lin. rewrite <- Ha, log2_nonpos; order. Qed. @@ -269,8 +268,8 @@ Lemma log2_mul_above : forall a b, 0<=a -> 0<=b -> log2 (a*b) <= log2 a + log2 b + 1. Proof. intros a b Ha Hb. - apply le_lteq in Ha. destruct Ha as [Ha|Ha]. - apply le_lteq in Hb. destruct Hb as [Hb|Hb]. + le_elim Ha. + le_elim Hb. apply lt_succ_r. rewrite add_1_r, <- add_succ_r, <- add_succ_l. apply log2_lt_pow2; try order_pos. @@ -432,11 +431,11 @@ Proof. apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. assert (H' : log2 b <= log2 (a+b)). apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - apply le_lteq in H. destruct H as [H|H]. + le_elim H. apply lt_le_trans with (log2 (a+b) + log2 b). now apply add_lt_mono_r. now apply add_le_mono_l. rewrite <- H at 1. apply add_lt_mono_l. - apply le_lteq in H'. destruct H' as [H'|H']. trivial. + le_elim H'; trivial. symmetry in H. apply log2_same in H; try order_pos. symmetry in H'. apply log2_same in H'; try order_pos. revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. @@ -534,7 +533,7 @@ Qed. Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a. Proof. intros a Ha. - apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + le_elim Ha. apply log2_up_unique; trivial. split; try order. apply pow_lt_mono_r; try order'. @@ -586,7 +585,7 @@ Lemma log2_log2_up_spec : forall a, 0<a -> Proof. intros a H. split. now apply log2_spec. - rewrite <-le_succ_l, <-one_succ, le_lteq in H. destruct H as [H|H]. + rewrite <-le_succ_l, <-one_succ in H. le_elim H. now apply log2_up_spec. now rewrite <-H, log2_up_1, pow_0_r. Qed. @@ -693,7 +692,7 @@ Qed. Lemma log2_up_le_lin : forall a, 0<=a -> log2_up a <= a. Proof. intros a Ha. - apply le_lteq in Ha; destruct Ha as [Ha|Ha]. + le_elim Ha. now apply lt_le_incl, log2_up_lt_lin. rewrite <- Ha, log2_up_nonpos; order. Qed. @@ -709,8 +708,8 @@ Proof. intros a b Ha Hb. assert (Ha':=log2_up_nonneg a). assert (Hb':=log2_up_nonneg b). - apply le_lteq in Ha. destruct Ha as [Ha|Ha]. - apply le_lteq in Hb. destruct Hb as [Hb|Hb]. + le_elim Ha. + le_elim Hb. apply log2_up_le_pow2; try order_pos. rewrite pow_add_r; trivial. apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'. @@ -722,8 +721,8 @@ Lemma log2_up_mul_below : forall a b, 0<a -> 0<b -> log2_up a + log2_up b <= S (log2_up (a*b)). Proof. intros a b Ha Hb. - rewrite <-le_succ_l, <-one_succ, le_lteq in Ha. destruct Ha as [Ha|Ha]. - rewrite <-le_succ_l, <-one_succ, le_lteq in Hb. destruct Hb as [Hb|Hb]. + rewrite <-le_succ_l, <-one_succ in Ha. le_elim Ha. + rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb. assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial). assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial). rewrite <- (lt_succ_pred 0 (log2_up a)); trivial. @@ -752,7 +751,7 @@ Lemma log2_up_mul_pow2 : forall a b, 0<a -> 0<=b -> log2_up (a*2^b) == b + log2_up a. Proof. intros a b Ha Hb. - rewrite <- le_succ_l, <- one_succ, le_lteq in Ha. destruct Ha as [Ha|Ha]. + rewrite <- le_succ_l, <- one_succ in Ha; le_elim Ha. apply log2_up_unique. apply add_nonneg_pos; trivial. now apply log2_up_pos. split. assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)). @@ -876,11 +875,11 @@ Proof. apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. assert (H' : log2_up b <= log2_up (a+b)). apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - apply le_lteq in H. destruct H as [H|H]. + le_elim H. apply lt_le_trans with (log2_up (a+b) + log2_up b). now apply add_lt_mono_r. now apply add_le_mono_l. rewrite <- H at 1. apply add_lt_mono_l. - apply le_lteq in H'. destruct H' as [H'|H']. trivial. + le_elim H'. trivial. symmetry in H. apply log2_up_same in H; try order_pos. symmetry in H'. apply log2_up_same in H'; try order_pos. revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 323ecef1b..3cd78351d 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -24,17 +24,16 @@ Qed. Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m). Proof. -nzord_induct p. -intros n m H; false_hyp H lt_irrefl. -intros p H IH n m H1. nzsimpl. -le_elim H. assert (LR : forall n m, n < m -> p * n + n < p * m + m). -intros n1 m1 H2. apply add_lt_mono; [now apply -> IH | assumption]. -split; [apply LR |]. intro H2. apply -> lt_dne; intro H3. -apply <- le_ngt in H3. le_elim H3. -apply lt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 lt_irrefl. -rewrite <- H; now nzsimpl. -intros p H1 _ n m H2. destruct (lt_asymm _ _ H1 H2). +intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). solve_proper. +intros. now nzsimpl. +clear p Hp. intros p Hp IH n m. nzsimpl. +assert (LR : forall n m, n < m -> p * n + n < p * m + m) + by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH). +split; intros H. +now apply LR. +destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. +rewrite EQ in H. order. +apply LR in GT. order. Qed. Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p). @@ -46,19 +45,19 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. nzord_induct p. -intros n m H; false_hyp H lt_irrefl. -intros p H1 _ n m H2. apply lt_succ_l in H2. apply <- nle_gt in H2. -false_hyp H1 H2. -intros p H IH n m H1. apply <- le_succ_l in H. -le_elim H. assert (LR : forall n m, n < m -> p * m < p * n). -intros n1 m1 H2. apply (le_lt_add_lt n1 m1). -now apply lt_le_incl. rewrite <- 2 mul_succ_l. now apply -> IH. -split; [apply LR |]. intro H2. apply -> lt_dne; intro H3. -apply <- le_ngt in H3. le_elim H3. -apply lt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 lt_irrefl. -rewrite (mul_lt_pred p (S p)) by reflexivity. -rewrite H; do 2 rewrite mul_0_l; now do 2 rewrite add_0_l. +order. +intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. +intros p Hp IH n m _. apply le_succ_l in Hp. +le_elim Hp. +assert (LR : forall n m, n < m -> p * m < p * n). + intros n1 m1 H. apply (le_lt_add_lt n1 m1). + now apply lt_le_incl. rewrite <- 2 mul_succ_l. now rewrite <- IH. +split; intros H. +now apply LR. +destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. +rewrite EQ in H. order. +apply LR in GT. order. +rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl. Qed. Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p). @@ -70,7 +69,7 @@ Qed. Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_pos_l. +le_elim H2. apply lt_le_incl. now apply mul_lt_mono_pos_l. apply eq_le_incl; now rewrite H2. apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l. Qed. @@ -78,7 +77,7 @@ Qed. Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_neg_l. +le_elim H2. apply lt_le_incl. now apply mul_lt_mono_neg_l. apply eq_le_incl; now rewrite H2. apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l. Qed. @@ -97,20 +96,13 @@ Qed. Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m). Proof. -intros n m p H; split; intro H1. -destruct (lt_trichotomy p 0) as [H2 | [H2 | H2]]. -apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * m < p * n); [now apply -> mul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 lt_irrefl. -assert (H4 : p * n < p * m); [now apply -> mul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 lt_irrefl. -false_hyp H2 H. -apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * n < p * m) by (now apply -> mul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 lt_irrefl. -assert (H4 : p * m < p * n) by (now apply -> mul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 lt_irrefl. -now rewrite H1. +intros n m p Hp; split; intro H; [|now apply mul_wd]. +apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp]; + destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. +apply (mul_lt_mono_neg_l p) in LT; order. +apply (mul_lt_mono_neg_l p) in GT; order. +apply (mul_lt_mono_pos_l p) in LT; order. +apply (mul_lt_mono_pos_l p) in GT; order. Qed. Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m). @@ -181,17 +173,17 @@ Qed. Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_pos_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_pos_r. Qed. Theorem mul_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r. Qed. Theorem mul_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r. Qed. Theorem mul_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0. @@ -206,7 +198,7 @@ Qed. Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m. Proof. -intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1. +intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1. rewrite mul_1_l in H1. now apply lt_1_l with m. assumption. Qed. @@ -227,7 +219,7 @@ Qed. Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof. intros n m; split; intro H. -intro H1; apply -> eq_mul_0 in H1. tauto. +intro H1; apply eq_mul_0 in H1. tauto. split; intro H1; rewrite H1 in H; (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H. Qed. @@ -239,13 +231,13 @@ Qed. Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0. Proof. -intros n m H1 H2. apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1]. +intros n m H1 H2. apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. assumption. false_hyp H1 H2. Qed. Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0. Proof. -intros n m H1 H2; apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1]. +intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. false_hyp H1 H2. assumption. Qed. @@ -281,18 +273,16 @@ Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). now apply lt_le_trans with 0. -destruct (lt_ge_cases n m). -assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonneg. -apply -> le_ngt in F. false_hyp H2 F. +destruct (lt_ge_cases n m) as [LT|LE]; trivial. +apply square_le_mono_nonneg in LE; order. Qed. Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). apply lt_le_incl; now apply lt_le_trans with 0. -destruct (le_gt_cases n m). -assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonneg. -apply -> lt_nge in F. false_hyp H2 F. +destruct (le_gt_cases n m) as [LE|LT]; trivial. +apply square_lt_mono_nonneg in LT; order. Qed. Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index ef9057c06..3722d4727 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -15,19 +15,19 @@ Module Type NZOrderProp Instance le_wd : Proper (eq==>eq==>iff) le. Proof. -intros n n' Hn m m' Hm. rewrite !lt_eq_cases, !Hn, !Hm; auto with *. +intros n n' Hn m m' Hm. now rewrite <- !lt_succ_r, Hn, Hm. Qed. Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H]. Theorem lt_le_incl : forall n m, n < m -> n <= m. Proof. -intros; apply <- lt_eq_cases; now left. +intros. apply lt_eq_cases. now left. Qed. Theorem le_refl : forall n, n <= n. Proof. -intro; apply <- lt_eq_cases; now right. +intro. apply lt_eq_cases. now right. Qed. Theorem lt_succ_diag_r : forall n, n < S n. @@ -97,7 +97,7 @@ intros n m; nzinduct n m. intros H; false_hyp H lt_irrefl. intro n; split; intros H H1 H2. apply lt_succ_r in H2. le_elim H2. -apply H; auto. apply -> le_succ_l. now apply lt_le_incl. +apply H; auto. apply le_succ_l. now apply lt_le_incl. rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l. apply le_succ_l in H1. le_elim H1. apply H; auto. rewrite lt_succ_r. now apply lt_le_incl. @@ -206,12 +206,12 @@ Qed. Theorem lt_succ_l : forall n m, S n < m -> n < m. Proof. -intros n m H; apply -> le_succ_l; order. +intros n m H; apply le_succ_l; order. Qed. Theorem le_le_succ_r : forall n m, n <= m -> n <= S m. Proof. -intros n m LE. rewrite <- lt_succ_r in LE. order. +intros n m LE. apply lt_succ_r in LE. order. Qed. Theorem lt_lt_succ_r : forall n m, n < m -> n < S m. @@ -254,15 +254,14 @@ Proof. apply lt_le_incl, lt_0_2. Qed. -Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m. -Proof. -intros n m H1 H2. rewrite one_succ. apply <- le_succ_l in H1. order. -Qed. - (** The order tactic enriched with some knowledge of 0,1,2 *) Ltac order' := generalize lt_0_1 lt_1_2; order. +Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m. +Proof. +intros n m H1 H2. rewrite <- le_succ_l, <- one_succ in H1. order. +Qed. (** More Trichotomy, decidability and double negation elimination. *) @@ -364,7 +363,7 @@ Proof. intro z; nzinduct n z. order. intro n; split; intros IH m H1 H2. -apply -> le_succ_r in H2. destruct H2 as [H2 | H2]. +apply le_succ_r in H2. destruct H2 as [H2 | H2]. now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2]. apply IH. assumption. now apply le_le_succ_r. Qed. @@ -414,14 +413,14 @@ Qed. Lemma rs'_rs'' : right_step' -> right_step''. Proof. intros RS' n; split; intros H1 m H2 H3. -apply -> lt_succ_r in H3; le_elim H3; +apply lt_succ_r in H3; le_elim H3; [now apply H1 | rewrite H3 in *; now apply RS']. apply H1; [assumption | now apply lt_lt_succ_r]. Qed. Lemma rbase : A' z. Proof. -intros m H1 H2. apply -> le_ngt in H1. false_hyp H2 H1. +intros m H1 H2. apply le_ngt in H1. false_hyp H2 H1. Qed. Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n. @@ -473,28 +472,28 @@ Let left_step'' := forall n, A' n <-> A' (S n). Lemma ls_ls' : A z -> left_step -> left_step'. Proof. intros Az LS n H1 H2. le_elim H1. -apply LS; trivial. apply H2; [now apply <- le_succ_l | now apply eq_le_incl]. +apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl]. rewrite H1; apply Az. Qed. Lemma ls'_ls'' : left_step' -> left_step''. Proof. intros LS' n; split; intros H1 m H2 H3. -apply -> le_succ_l in H3. apply lt_le_incl in H3. now apply H1. +apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1. le_elim H3. -apply <- le_succ_l in H3. now apply H1. +apply le_succ_l in H3. now apply H1. rewrite <- H3 in *; now apply LS'. Qed. Lemma lbase : A' (S z). Proof. -intros m H1 H2. apply -> le_succ_l in H2. -apply -> le_ngt in H1. false_hyp H2 H1. +intros m H1 H2. apply le_succ_l in H2. +apply le_ngt in H1. false_hyp H2 H1. Qed. Lemma A'A_left : (forall n, A' n) -> forall n, n <= z -> A n. Proof. -intros H1 n H2. apply H1 with (n := n); [assumption | now apply eq_le_incl]. +intros H1 n H2. apply (H1 n); [assumption | now apply eq_le_incl]. Qed. Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n. @@ -551,8 +550,8 @@ Theorem order_induction' : forall n, A n. Proof. intros Az AS AP n; apply order_induction; try assumption. -intros m H1 H2. apply AP in H2; [| now apply <- le_succ_l]. -apply -> (A_wd (P (S m)) m); [assumption | apply pred_succ]. +intros m H1 H2. apply AP in H2; [|now apply le_succ_l]. +now rewrite pred_succ in H2. Qed. End Center. @@ -579,8 +578,8 @@ Theorem lt_ind : forall (n : t), forall m, n < m -> A m. Proof. intros n H1 H2 m H3. -apply right_induction with (S n); [assumption | | now apply <- le_succ_l]. -intros; apply H2; try assumption. now apply -> le_succ_l. +apply right_induction with (S n); [assumption | | now apply le_succ_l]. +intros; apply H2; try assumption. now apply le_succ_l. Qed. (** Elimination principle for <= *) @@ -606,8 +605,8 @@ Section WF. Variable z : t. -Let Rlt (n m : t) := z <= n /\ n < m. -Let Rgt (n m : t) := m < n /\ n <= z. +Let Rlt (n m : t) := z <= n < m. +Let Rgt (n m : t) := m < n <= z. Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt. Proof. @@ -619,25 +618,13 @@ Proof. intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2. Qed. -Instance Acc_lt_wd : Proper (eq==>iff) (Acc Rlt). -Proof. -intros x1 x2 H; split; intro H1; destruct H1 as [H2]; -constructor; intros; apply H2; now (rewrite H || rewrite <- H). -Qed. - -Instance Acc_gt_wd : Proper (eq==>iff) (Acc Rgt). -Proof. -intros x1 x2 H; split; intro H1; destruct H1 as [H2]; -constructor; intros; apply H2; now (rewrite H || rewrite <- H). -Qed. - Theorem lt_wf : well_founded Rlt. Proof. unfold well_founded. apply strong_right_induction' with (z := z). -apply Acc_lt_wd. +auto with typeclass_instances. intros n H; constructor; intros y [H1 H2]. -apply <- nle_gt in H2. elim H2. now apply le_trans with z. +apply nle_gt in H2. elim H2. now apply le_trans with z. intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. Qed. @@ -645,11 +632,11 @@ Theorem gt_wf : well_founded Rgt. Proof. unfold well_founded. apply strong_left_induction' with (z := z). -apply Acc_gt_wd. +auto with typeclass_instances. intros n H; constructor; intros y [H1 H2]. -apply <- nle_gt in H2. elim H2. now apply le_lt_trans with n. +apply nle_gt in H2. elim H2. now apply le_lt_trans with n. intros n H1 H2; constructor; intros m [H3 H4]. -apply H2. assumption. now apply <- le_succ_l. +apply H2. assumption. now apply le_succ_l. Qed. End WF. @@ -662,4 +649,3 @@ End NZOrderProp. Module NZOrderedType (NZ : NZDecOrdSig') <: DecidableTypeFull <: OrderedTypeFull := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec. - diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 29b85724e..4287319e4 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -26,10 +26,10 @@ Module Type NZParityProp (** Morphisms *) Instance Even_wd : Proper (eq==>iff) Even. -Proof. unfold Even. solve_predicate_wd. Qed. +Proof. unfold Even. solve_proper. Qed. Instance Odd_wd : Proper (eq==>iff) Odd. -Proof. unfold Odd. solve_predicate_wd. Qed. +Proof. unfold Odd. solve_proper. Qed. Instance even_wd : Proper (eq==>Logic.eq) even. Proof. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 23c27777a..58704735f 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -69,7 +69,7 @@ Qed. Lemma pow_1_l : forall a, 0<=a -> 1^a == 1. Proof. - apply le_ind; intros. solve_predicate_wd. + apply le_ind; intros. solve_proper. now nzsimpl. now nzsimpl. Qed. @@ -88,7 +88,7 @@ Hint Rewrite pow_2_r : nz. Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0. Proof. intros a b Hb. apply le_ind with (4:=Hb). - solve_predicate_wd. + solve_proper. rewrite pow_0_r. order'. clear b Hb. intros b Hb IH. rewrite pow_succ_r by trivial. @@ -118,7 +118,7 @@ Qed. Lemma pow_add_r : forall a b c, 0<=b -> 0<=c -> a^(b+c) == a^b * a^c. Proof. - intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + intros a b c Hb. apply le_ind with (4:=Hb). solve_proper. now nzsimpl. clear b Hb. intros b Hb IH Hc. nzsimpl; trivial. @@ -132,7 +132,7 @@ Proof. intros a b c. destruct (lt_ge_cases c 0) as [Hc|Hc]. rewrite !(pow_neg_r _ _ Hc). now nzsimpl. - apply le_ind with (4:=Hc). solve_predicate_wd. + apply le_ind with (4:=Hc). solve_proper. now nzsimpl. clear c Hc. intros c Hc IH. nzsimpl; trivial. @@ -142,7 +142,7 @@ Qed. Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c -> a^(b*c) == (a^b)^c. Proof. - intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + intros a b c Hb. apply le_ind with (4:=Hb). solve_proper. intros. now nzsimpl. clear b Hb. intros b Hb IH Hc. nzsimpl; trivial. @@ -157,7 +157,7 @@ Proof. intros a b Ha. destruct (lt_ge_cases b 0) as [Hb|Hb]. now rewrite !(pow_neg_r _ _ Hb). - apply le_ind with (4:=Hb). solve_predicate_wd. + apply le_ind with (4:=Hb). solve_proper. nzsimpl; order'. clear b Hb. intros b Hb IH. nzsimpl; trivial. now apply mul_nonneg_nonneg. @@ -165,7 +165,7 @@ Qed. Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b. Proof. - intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper. nzsimpl; order'. clear b Hb. intros b Hb IH. nzsimpl; trivial. now apply mul_pos_pos. @@ -175,7 +175,7 @@ Qed. Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c. Proof. - intros a b c Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + intros a b c Hc. apply lt_ind with (4:=Hc). solve_proper. intros (Ha,H). nzsimpl; trivial; order. clear c Hc. intros c Hc IH (Ha,H). nzsimpl; try order. @@ -327,7 +327,7 @@ Qed. Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b. Proof. - intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd. + intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper. nzsimpl. order'. clear b Hb. intros b Hb IH. nzsimpl; trivial. rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha. @@ -347,7 +347,7 @@ Qed. Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c -> a^c + b^c <= (a+b)^c. Proof. - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper. nzsimpl; order. clear c Hc. intros c Hc IH. assert (0<=c) by order'. @@ -387,7 +387,7 @@ Proof. apply mul_le_mono_nonneg_l; trivial. apply pow_le_mono_l; try split; order. (* end *) - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd. + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper. nzsimpl; order. clear c Hc. intros c Hc IH. assert (0<=c) by order. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 414770d18..8b6dcc3d6 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder. (** Interface of a sqrt function, then its specification on naturals *) Module Type Sqrt (Import A : Typ). - Parameters Inline sqrt : t -> t. + Parameter Inline sqrt : t -> t. End Sqrt. Module Type SqrtNotation (A : Typ)(Import B : Sqrt A). @@ -460,7 +460,7 @@ Qed. Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a. Proof. intros a Ha. - apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + le_elim Ha. rewrite sqrt_up_eqn by (now apply mul_pos_pos). rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial. rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl. @@ -516,7 +516,7 @@ Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)². Proof. intros a H. split. now apply sqrt_spec. - rewrite le_lteq in H. destruct H as [H|H]. + le_elim H. now apply sqrt_up_spec. now rewrite <-H, sqrt_up_0, mul_0_l. Qed. @@ -596,7 +596,7 @@ Qed. Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a. Proof. intros a Ha. - apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + le_elim Ha. rewrite sqrt_up_eqn; trivial. apply le_succ_l. apply le_lt_trans with (P a). apply sqrt_le_lin. now rewrite <- lt_succ_r, (lt_succ_pred 0). @@ -670,7 +670,7 @@ Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a -> Proof. intros a Ha. split. intros EQ. - apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + le_elim Ha. exists (√°a). split. apply sqrt_up_nonneg. generalize (proj2 (sqrt_up_spec a Ha)). assert (Ha' : 0 < S a) by (apply lt_succ_r; order'). @@ -710,8 +710,8 @@ Qed. Lemma add_sqrt_up_le : forall a b, 0<=a -> 0<=b -> √°a + √°b <= S √°(2*(a+b)). Proof. intros a b Ha Hb. - apply le_lteq in Ha; destruct Ha as [Ha|Ha]. - apply le_lteq in Hb; destruct Hb as [Hb|Hb]. + le_elim Ha. + le_elim Hb. rewrite 3 sqrt_up_eqn; trivial. nzsimpl. rewrite <- 2 succ_le_mono. etransitivity; [eapply add_sqrt_le|]. diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index fbe71a4c7..72e09f157 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -22,9 +22,9 @@ intros n m; induct n. nzsimpl; intuition. intros n IH. nzsimpl. setoid_replace (S (n + m) == 0) with False by - (apply -> neg_false; apply neq_succ_0). + (apply neg_false; apply neq_succ_0). setoid_replace (S n == 0) with False by - (apply -> neg_false; apply neq_succ_0). tauto. + (apply neg_false; apply neq_succ_0). tauto. Qed. Theorem eq_add_succ : @@ -47,11 +47,11 @@ Theorem eq_add_1 : forall n m, Proof. intros n m. rewrite one_succ. intro H. assert (H1 : exists p, n + m == S p) by now exists 0. -apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. +apply eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H. -apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. +apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H. -apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. +apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. Qed. Theorem succ_add_discr : forall n m, m ~= S (n + m). diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 7ed563be5..ac8a05220 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -41,7 +41,7 @@ nzinduct n. now apply eq_le_incl. intro n; split. apply le_le_succ_r. -intro H; apply -> le_succ_r in H; destruct H as [H | H]. +intro H; apply le_succ_r in H; destruct H as [H | H]. assumption. symmetry in H; false_hyp H neq_succ_0. Qed. @@ -179,7 +179,7 @@ Ltac double_induct n m := try intros until n; try intros until m; pattern n, m; apply double_induction; clear n m; - [solve_relation_wd | | | ]. + [solve_proper | | | ]. End NBaseProp. diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 2cb5bbc06..70f6f7945 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -303,7 +303,7 @@ Qed. Lemma bits_inj : forall a b, testbit a === testbit b -> a == b. Proof. intros a. pattern a. - apply strong_right_induction with 0;[solve_predicate_wd|clear a|apply le_0_l]. + apply strong_right_induction with 0;[solve_proper|clear a|apply le_0_l]. intros a _ IH b H. destruct (eq_0_gt_0_cases a) as [EQ|LT]. rewrite EQ in H |- *. symmetry. apply bits_inj_0. @@ -342,7 +342,7 @@ Proof. exists 0. intros m. rewrite bits_0, H0; trivial. apply le_0_l. intros k IH f Hf Hk. destruct (IH (fun m => f (S m))) as (n, Hn). - solve_predicate_wd. + solve_proper. intros m Hm. apply Hk. now rewrite <- succ_le_mono. exists (f 0 + 2*n). intros m. destruct (zero_or_succ m) as [Hm|(m', Hm)]; rewrite Hm. diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v index 1340e5124..1192e5cdc 100644 --- a/theories/Numbers/Natural/Abstract/NGcd.v +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -97,11 +97,11 @@ Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m -> Proof. intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. pattern n. apply strong_right_induction with (z:=1); trivial. - unfold Bezout. solve_predicate_wd. + 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. - unfold Bezout. solve_predicate_wd. + unfold Bezout. solve_proper. clear m Hm. intros m Hm IHm. destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. (* n < m *) @@ -191,8 +191,7 @@ Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) -> exists q r, n == q*r /\ (q | m) /\ (r | p). Proof. intros n m p Hn H. - assert (G := gcd_nonneg n m). - apply le_lteq in G; destruct G as [G|G]. + assert (G := gcd_nonneg n m). le_elim G. destruct (gcd_divide_l n m) as (q,Hq). exists (gcd n m). exists q. split. easy. diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index f3b45e308..8a1a4def6 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -192,8 +192,8 @@ Lemma lcm_unique_alt : forall n m p, 0<=p -> Proof. intros n m p Hp H. apply lcm_unique; trivial. - apply -> H. apply divide_refl. - apply -> H. apply divide_refl. + apply H, divide_refl. + apply H, divide_refl. intros. apply H. now split. Qed. diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index 6ecdef9ef..804d1ccc0 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -53,7 +53,7 @@ Qed. Theorem lt_0_mul' : forall n m, n * m > 0 <-> n > 0 /\ m > 0. Proof. intros n m; split; [intro H | intros [H1 H2]]. -apply -> lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. +apply lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. now apply mul_pos_pos. Qed. @@ -65,11 +65,11 @@ Proof. intros n m. split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. intro H; destruct (lt_trichotomy n 1) as [H1 | [H1 | H1]]. -apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. order'. +apply lt_1_r in H1. rewrite H1, mul_0_l in H. order'. rewrite H1, mul_1_l in H; now split. destruct (eq_0_gt_0_cases m) as [H2 | H2]. rewrite H2, mul_0_r in H. order'. -apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. +apply (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. assert (H3 : 1 < n * m) by now apply (lt_1_l m). rewrite H in H3; false_hyp H3 lt_irrefl. Qed. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 2816af7c4..8bba7d72b 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -17,7 +17,7 @@ Include NAddProp N. Theorem lt_wf_0 : well_founded lt. Proof. -setoid_replace lt with (fun n m => 0 <= n /\ n < m). +setoid_replace lt with (fun n m => 0 <= n < m). apply lt_wf. intros x y; split. intro H; split; [apply le_0_l | assumption]. now intros [_ H]. @@ -27,12 +27,12 @@ Defined. Theorem nlt_0_r : forall n, ~ n < 0. Proof. -intro n; apply -> le_ngt. apply le_0_l. +intro n; apply le_ngt. apply le_0_l. Qed. Theorem nle_succ_0 : forall n, ~ (S n <= 0). Proof. -intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r. +intros n H; apply le_succ_l in H; false_hyp H nlt_0_r. Qed. Theorem le_0_r : forall n, n <= 0 <-> n == 0. @@ -118,9 +118,9 @@ Proof. intros Base Step; induct n. intros; apply Base. intros n IH m H. elim H using le_ind. -solve_predicate_wd. +solve_proper. apply Step; [| apply IH]; now apply eq_le_incl. -intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto. +intros k H1 H2. apply le_succ_l in H1. apply lt_le_incl in H1. auto. Qed. Theorem lt_ind_rel : @@ -132,7 +132,7 @@ intros Base Step; 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. -solve_predicate_wd. +solve_proper. apply Step; [| apply IH]; now apply lt_succ_diag_r. intros k H1 H2. apply lt_succ_l in H1. auto. Qed. @@ -176,7 +176,7 @@ Theorem lt_le_pred : forall n m, n < m -> n <= P m. Proof. intro n; cases m. intro H; false_hyp H nlt_0_r. -intros m IH. rewrite pred_succ; now apply -> lt_succ_r. +intros m IH. rewrite pred_succ; now apply lt_succ_r. Qed. Theorem lt_pred_le : forall n m, P n < m -> n <= m. @@ -184,7 +184,7 @@ Theorem lt_pred_le : forall n m, P n < m -> n <= m. Proof. intros n m; cases n. rewrite pred_0; intro H; now apply lt_le_incl. -intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l. +intros n IH. rewrite pred_succ in IH. now apply le_succ_l. Qed. Theorem lt_pred_lt : forall n m, n < P m -> n < m. @@ -201,7 +201,7 @@ Theorem pred_le_mono : forall n m, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *) Proof. intros n m H; elim H using le_ind_rel. -solve_relation_wd. +solve_proper. intro; rewrite pred_0; apply le_0_l. intros p q H1 _; now do 2 rewrite pred_succ. Qed. @@ -209,12 +209,12 @@ Qed. Theorem pred_lt_mono : forall n m, 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. +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 ; -[apply <- succ_lt_mono | | |]. -assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n). +[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. -apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. +apply succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. Qed. Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m. @@ -225,13 +225,13 @@ Qed. Theorem le_succ_le_pred : forall n m, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply lt_le_pred. now apply -> le_succ_l. +intros n m H. apply lt_le_pred. now apply le_succ_l. Qed. Theorem lt_pred_lt_succ : forall n m, P n < m -> n < S m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply <- lt_succ_r. now apply lt_pred_le. +intros n m H. apply lt_succ_r. now apply lt_pred_le. Qed. Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m. diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v index 68976624e..67ed77981 100644 --- a/theories/Numbers/Natural/Abstract/NPow.v +++ b/theories/Numbers/Natural/Abstract/NPow.v @@ -146,7 +146,7 @@ Proof. wrap pow_add_upper. Qed. Lemma even_pow : forall a b, b~=0 -> even (a^b) = even a. Proof. intros a b Hb. rewrite neq_0_lt_0 in Hb. - apply lt_ind with (4:=Hb). solve_predicate_wd. + apply lt_ind with (4:=Hb). solve_proper. now nzsimpl. clear b Hb. intros b Hb IH. rewrite pow_succ_r', even_mul, IH. now destruct (even a). diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index 4232ecbfa..d7143c677 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -35,7 +35,7 @@ Qed. Theorem sub_gt : forall n m, n > m -> n - m ~= 0. Proof. intros n m H; elim H using lt_ind_rel; clear n m H. -solve_relation_wd. +solve_proper. intro; rewrite sub_0_r; apply neq_succ_0. intros; now rewrite sub_succ. Qed. @@ -45,8 +45,8 @@ Proof. intros n m p; induct p. intro; now do 2 rewrite sub_0_r. intros p IH H. do 2 rewrite sub_succ_r. -rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). -rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l). +rewrite <- IH by (apply lt_le_incl; now apply le_succ_l). +rewrite add_pred_r by (apply sub_gt; now apply le_succ_l). reflexivity. Qed. @@ -242,10 +242,10 @@ intros n IH. destruct (le_gt_cases m n) as [H | H]. rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. -now apply <- add_cancel_l. -assert (H1 : S n <= m); [now apply <- le_succ_l |]. -setoid_replace (S n - m) with 0 by now apply <- sub_0_le. -setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r). +now apply add_cancel_l. +assert (H1 : S n <= m); [now apply le_succ_l |]. +setoid_replace (S n - m) with 0 by now apply sub_0_le. +setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r). apply mul_0_l. Qed. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index d2979bcf0..82380e9b4 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -77,7 +77,7 @@ Theorem min_r : forall n m, m <= n -> Nmin n m = m. Proof. unfold Nmin, Nle; intros n m H. case_eq (n ?= m); intro H1; try reflexivity. -now apply -> Ncompare_eq_correct. +now apply Ncompare_eq_correct. rewrite <- Ncompare_antisym, H1 in H; elim H; auto. Qed. @@ -85,7 +85,7 @@ Theorem max_l : forall n m, m <= n -> Nmax n m = n. Proof. unfold Nmax, Nle; intros n m H. case_eq (n ?= m); intro H1; try reflexivity. -symmetry; now apply -> Ncompare_eq_correct. +symmetry; now apply Ncompare_eq_correct. rewrite <- Ncompare_antisym, H1 in H; elim H; auto. Qed. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 79f487efc..ba7859ee4 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -8,130 +8,17 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Export Setoid Morphisms. +Require Export Setoid Morphisms Morphisms_Prop. Set Implicit Arguments. -(* -Contents: -- Coercion from bool to Prop -- Extension of the tactics stepl and stepr -- Extentional properties of predicates, relations and functions - (well-definedness and equality) -- Relations on cartesian product -- Miscellaneous -*) -(** Coercion from bool to Prop *) - -(*Definition eq_bool := (@eq bool).*) - -(*Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.*) -(* This has been added to theories/Datatypes.v *) -(*Coercion eq_true : bool >-> Sortclass.*) - -(*Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true. -Proof. -intro b; split; intro H. now inversion H. now rewrite H. -Qed. - -Theorem eq_true_unfold_neg : forall b : bool, ~ b <-> b = false. -Proof. -intros b; destruct b; simpl; rewrite eq_true_unfold_pos. -split; intro H; [elim (H (refl_equal true)) | discriminate H]. -split; intro H; [reflexivity | discriminate]. -Qed. - -Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2. -Proof. -destruct b1; destruct b2; simpl; tauto. -Qed. - -Theorem eq_true_and : forall b1 b2 : bool, b1 && b2 <-> b1 /\ b2. -Proof. -destruct b1; destruct b2; simpl; tauto. -Qed. - -Theorem eq_true_neg : forall b : bool, negb b <-> ~ b. -Proof. -destruct b; simpl; rewrite eq_true_unfold_pos; rewrite eq_true_unfold_neg; -split; now intro. -Qed. - -Theorem eq_true_iff : forall b1 b2 : bool, b1 = b2 <-> (b1 <-> b2). -Proof. -intros b1 b2; split; intro H. -now rewrite H. -destruct b1; destruct b2; simpl; try reflexivity. -apply -> eq_true_unfold_neg. rewrite H. now intro. -symmetry; apply -> eq_true_unfold_neg. rewrite <- H; now intro. -Qed.*) - -(** Extension of the tactics stepl and stepr to make them -applicable to hypotheses *) - -Tactic Notation "stepl" constr(t1') "in" hyp(H) := -match (type of H) with -| ?R ?t1 ?t2 => - let H1 := fresh in - cut (R t1' t2); [clear H; intro H | stepl t1; [assumption |]] -| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)" -end. - -Tactic Notation "stepl" constr(t1') "in" hyp(H) "by" tactic(r) := stepl t1' in H; [| r]. - -Tactic Notation "stepr" constr(t2') "in" hyp(H) := -match (type of H) with -| ?R ?t1 ?t2 => - let H1 := fresh in - cut (R t1 t2'); [clear H; intro H | stepr t2; [assumption |]] -| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)" -end. - -Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r]. - -(** Predicates, relations, functions *) - -Definition predicate (A : Type) := A -> Prop. - -Instance well_founded_wd A : - Proper (@relation_equivalence A ==> iff) (@well_founded A). -Proof. -intros R1 R2 H. -split; intros WF a; induction (WF a) as [x _ WF']; constructor; -intros y Ryx; apply WF'; destruct (H y x); auto. -Qed. - -(** [solve_predicate_wd] solves the goal [Proper (?==>iff) P] - for P consisting of morphisms and quantifiers *) - -Ltac solve_predicate_wd := -let x := fresh "x" in -let y := fresh "y" in -let H := fresh "H" in - intros x y H; setoid_rewrite H; reflexivity. - -(** [solve_relation_wd] solves the goal [Proper (?==>?==>iff) R] - for R consisting of morphisms and quantifiers *) - -Ltac solve_relation_wd := -let x1 := fresh "x" in -let y1 := fresh "y" in -let H1 := fresh "H" in -let x2 := fresh "x" in -let y2 := fresh "y" in -let H2 := fresh "H" in - intros x1 y1 H1 x2 y2 H2; - rewrite H1; setoid_rewrite H2; reflexivity. - -(* The following tactic uses solve_predicate_wd to solve the goals -relating to well-defidedness that are produced by applying induction. +(* The following tactic uses solve_proper to solve the goals +relating to well-definedness that are produced by applying induction. We declare it to take the tactic that applies the induction theorem and not the induction theorem itself because the tactic may, for example, supply additional arguments, as does NZinduct_center in NZBase.v *) Ltac induction_maker n t := - try intros until n; - pattern n; t; clear n; - [solve_predicate_wd | ..]. + try intros until n; pattern n; t; clear n; [solve_proper | ..]. |