diff options
| -rw-r--r-- | theories/Lists/List.v | 42 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 10 | ||||
| -rw-r--r-- | theories/NArith/Ndist.v | 57 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 186 | ||||
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 39 | ||||
| -rw-r--r-- | theories/ZArith/Zdigits.v | 5 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 20 | ||||
| -rw-r--r-- | theories/ZArith/Zgcd_alt.v | 3 |
8 files changed, 133 insertions, 229 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 4850b3c4c..3e660caab 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -227,10 +227,8 @@ Section Facts. intros. injection H. intro. - cut ([] = l ++ a0 :: l0); auto. - intro. - generalize (app_cons_not_nil _ _ _ H1); intro. - elim H2. + assert ([] = l ++ a0 :: l0) by auto. + apply app_cons_not_nil in H1 as []. Qed. Lemma app_inj_tail : @@ -239,22 +237,20 @@ Section Facts. induction x as [| x l IHl]; [ destruct y as [| a l] | destruct y as [| a l0] ]; simpl; auto. - intros a b H. - injection H. - auto. - intros a0 b H. - injection H; intros. - generalize (app_cons_not_nil _ _ _ H0); destruct 1. - intros a b H. - injection H; intros. - cut ([] = l ++ [a]); auto. - intro. - generalize (app_cons_not_nil _ _ _ H2); destruct 1. - intros a0 b H. - injection H; intros. - destruct (IHl l0 a0 b H0). - split; auto. - rewrite <- H1; rewrite <- H2; reflexivity. + - intros a b H. + injection H. + auto. + - intros a0 b H. + injection H as H1 H0. + apply app_cons_not_nil in H0 as []. + - intros a b H. + injection H as H1 H0. + assert ([] = l ++ [a]) by auto. + apply app_cons_not_nil in H as []. + - intros a0 b H. + injection H as <- H0. + destruct (IHl l0 a0 b H0) as (<-,<-). + split; auto. Qed. @@ -1003,10 +999,8 @@ End Fold_Left_Recursor. Lemma fold_left_length : forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l. Proof. - intro A. - cut (forall (l:list A) n, fold_left (fun x _ => S x) l n = n + length l). - intros. - exact (H l 0). + 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. intros; rewrite IHl. simpl; auto with arith. diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index f8db75484..6c9a03a65 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -119,11 +119,11 @@ Lemma Nneq_elim a a' : N.odd a = negb (N.odd a') \/ N.eqb (N.div2 a) (N.div2 a') = false. Proof. - intros. cut (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')). - intros. elim H0. intro. right. apply Ndiv2_bit_neq. assumption. - assumption. - intro. left. assumption. - case (N.odd a), (N.odd a'); auto. + intros. + enough (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')) as []. + - right. apply Ndiv2_bit_neq; assumption. + - left. assumption. + - case (N.odd a), (N.odd a'); auto. Qed. Lemma Ndouble_or_double_plus_un a : diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index ce4f76634..b340d5fd0 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -71,7 +71,7 @@ Proof. auto with bool arith. intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3. intros. simpl. unfold Nplength in H. - cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity. + enough (ni (Pplength p0) = ni n0) by (inversion H4; reflexivity). apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false). apply H2. apply lt_n_S. exact H4. exact H3. intro. case n. trivial. @@ -104,10 +104,9 @@ Lemma ni_min_comm : forall d d':natinf, ni_min d d' = ni_min d' d. Proof. simple induction d. simple induction d'; trivial. simple induction d'; trivial. elim n. simple induction n0; trivial. - intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0). - intro. unfold ni_min. simpl. rewrite H1. reflexivity. - cut (ni (min n0 n2) = ni (min n2 n0)). intros. - inversion H1; trivial. + intros. elim n1; trivial. intros. unfold ni_min in H. + enough (min n0 n2 = min n2 n0) by (unfold ni_min; simpl; rewrite H1; reflexivity). + enough (ni (min n0 n2) = ni (min n2 n0)) by (inversion H1; trivial). exact (H n2). Qed. @@ -116,10 +115,10 @@ Lemma ni_min_assoc : Proof. simple induction d; trivial. simple induction d'; trivial. simple induction d''; trivial. - unfold ni_min. intro. cut (min (min n n0) n1 = min n (min n0 n1)). - intro. rewrite H. reflexivity. - generalize n0 n1. elim n; trivial. - simple induction n3; trivial. simple induction n5; trivial. + unfold ni_min. intro. + enough (min (min n n0) n1 = min n (min n0 n1)) by (rewrite H; reflexivity). + induction n in n0, n1 |- *; trivial. + destruct n0; trivial. destruct n1; trivial. intros. simpl. auto. Qed. @@ -174,15 +173,13 @@ Qed. Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'. Proof. - simple induction d. intro. right. exact (ni_min_inf_l d'). - simple induction d'. left. exact (ni_min_inf_r (ni n)). - unfold ni_min. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). - intros. case (H n0). intro. left. rewrite H0. reflexivity. - intro. right. rewrite H0. reflexivity. - elim n. intro. left. reflexivity. - simple induction n1. right. reflexivity. - intros. case (H n2). intro. left. simpl. rewrite H1. reflexivity. - intro. right. simpl. rewrite H1. reflexivity. + destruct d. right. exact (ni_min_inf_l d'). + destruct d'. left. exact (ni_min_inf_r (ni n)). + unfold ni_min. + enough (min n n0 = n \/ min n n0 = n0) as [-> | ->]. + left. reflexivity. + right. reflexivity. + destruct (Nat.min_dec n n0); [left|right]; assumption. Qed. Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d. @@ -208,11 +205,7 @@ Qed. Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n). Proof. - cut (forall m n:nat, m <= n -> min m n = m). - intros. unfold ni_le, ni_min. rewrite (H m n H0). reflexivity. - simple induction m. trivial. - simple induction n0. intro. inversion H0. - intros. simpl. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. + intros * H. unfold ni_le, ni_min. rewrite (Peano.min_l m n H). reflexivity. Qed. Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n. @@ -298,30 +291,28 @@ Proof. rewrite (ni_min_inf_l (Nplength a')) in H. rewrite (Nplength_infty a' H). simpl. apply ni_le_refl. intros. unfold Nplength at 1. apply Nplength_lb. intros. - cut (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false). - intros. apply H1. reflexivity. + enough (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false). + { apply H1. reflexivity. } intro a''. case a''. intro. reflexivity. intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). rewrite (Nplength_zeros (Npos p) (Pplength p) (eq_refl (Nplength (Npos p))) k H0). - generalize H. case a'. trivial. - intros. cut (N.testbit_nat (Npos p1) k = false). intros. rewrite H3. reflexivity. + destruct a'. trivial. + enough (N.testbit_nat (Npos p1) k = false) as -> by reflexivity. apply Nplength_zeros with (n := Pplength p1). reflexivity. apply (lt_le_trans k (Pplength p) (Pplength p1)). exact H0. - apply ni_le_le. exact H2. + apply ni_le_le. exact H. Qed. Lemma Nplength_ultra : forall a a':N, ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')). Proof. - intros. case (ni_le_total (Nplength a) (Nplength a')). intro. - cut (ni_min (Nplength a) (Nplength a') = Nplength a). - intro. rewrite H0. apply Nplength_ultra_1. exact H. + intros. destruct (ni_le_total (Nplength a) (Nplength a')). + enough (ni_min (Nplength a) (Nplength a') = Nplength a) as -> by (apply Nplength_ultra_1; exact H). exact H. - intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a'). - intro. rewrite H0. rewrite N.lxor_comm. apply Nplength_ultra_1. exact H. + enough (ni_min (Nplength a) (Nplength a') = Nplength a') as -> by (rewrite N.lxor_comm; apply Nplength_ultra_1; exact H). rewrite ni_min_comm. exact H. Qed. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index d5e807f5a..b64d7f290 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -75,16 +75,12 @@ Section Wf_Lexicographic_Exponentiation. Proof. intros. inversion H. - generalize (app_cons_not_nil _ _ _ H1); simple induction 1. - cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets. - intro. - generalize (app_eq_unit _ _ H0). - simple induction 1; simple induction 1; intros. - rewrite H4; auto using d_nil with sets. - discriminate H5. - generalize (app_inj_tail _ _ _ _ H0). - simple induction 1; intros. - rewrite <- H4; auto with sets. + - apply app_cons_not_nil in H1 as []. + - assert (x ++ Cons a Nil = Cons x0 Nil) by auto with sets. + apply app_eq_unit in H0 as [(->,_)|(_,[=])]. + auto using d_nil. + - apply app_inj_tail in H0 as (<-,_). + assumption. Qed. Lemma desc_tail : @@ -93,53 +89,25 @@ Section Wf_Lexicographic_Exponentiation. Proof. intro. apply rev_ind with - (A := A) (P := fun x:List => forall a b:A, - Descl (Cons b (x ++ Cons a Nil)) -> clos_refl_trans A leA a b). - intros. - - inversion H. - cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil); - auto with sets; intro. - generalize H0. - intro. - generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4); - simple induction 1. - intros. - - generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. - generalize H1. - rewrite <- H10; rewrite <- H7; intro. - inversion H11; subst; [apply rt_step; assumption|apply rt_refl]. - - intros. - inversion H0. - generalize (app_cons_not_nil _ _ _ H3); intro. - elim H1. - - generalize H0. - generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b); - simple induction 1. - intro. - generalize (desc_prefix (Cons b (l ++ Cons x0 Nil)) a H5); intro. - generalize (H x0 b H6). - intro. - apply rt_trans with (A := A) (y := x0); auto with sets. - - match goal with [ |- clos_refl_trans ?A ?R ?x ?y ] => cut (clos_refl A R x y) end. - intros; inversion H8; subst; [apply rt_step|apply rt_refl]; assumption. - generalize H1. - setoid_rewrite H4; intro. - - generalize (app_inj_tail _ _ _ _ H8); simple induction 1. - intros. - generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b). - intro. - generalize H10. - rewrite H12; intro. - generalize (app_inj_tail _ _ _ _ H13); simple induction 1. - intros; subst; assumption. + Descl (Cons b (x ++ Cons a Nil)) -> clos_refl_trans A leA a b); intros. + - inversion H. + assert (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil) by + auto with sets. + destruct (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H0) as (H6,<-). + apply app_inj_tail in H6 as (?,<-). + inversion H1; subst; [apply rt_step; assumption|apply rt_refl]. + - inversion H0. + + apply app_cons_not_nil in H3 as []. + + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0. + pose proof (H x0 b H0). + apply rt_trans with (y := x0); auto with sets. + enough (H5:clos_refl A leA a x0) by (inversion H5; subst; [apply rt_step|apply rt_refl]; assumption). + apply app_inj_tail in H1 as (H1,->). + rewrite app_comm_cons in H1. + apply app_inj_tail in H1 as (_,<-). + assumption. Qed. @@ -147,82 +115,38 @@ Section Wf_Lexicographic_Exponentiation. forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y. Proof. intros z D. - elim D. - intros. - cut (x ++ y = Nil); auto with sets; intro. - generalize (app_eq_nil _ _ H0); simple induction 1. - intros. - rewrite H2; rewrite H3; split; apply d_nil. - - intros. - cut (x0 ++ y = Cons x Nil); auto with sets. - intros E. - generalize (app_eq_unit _ _ E); simple induction 1. - simple induction 1; intros. - rewrite H2; rewrite H3; split. - apply d_nil. - - apply d_one. - - simple induction 1; intros. - rewrite H2; rewrite H3; split. - apply d_one. - - apply d_nil. - - do 5 intro. - intros Hind. - do 2 intro. - generalize x0. - apply rev_ind with - (A := A) - (P := fun y0:List => - forall x0:List, - (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 -> - Descl x0 /\ Descl y0). - - intro. - generalize (app_nil_end x1). - simple induction 1; simple induction 1. - split. apply d_conc; auto with sets. - - apply d_nil. - - do 3 intro. - generalize x1. - apply rev_ind with - (A := A) - (P := fun l0:List => - forall (x1:A) (x0:List), - (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ l0 ++ Cons x1 Nil -> - Descl x0 /\ Descl (l0 ++ Cons x1 Nil)). - - - simpl. - split. - generalize (app_inj_tail _ _ _ _ H2); simple induction 1. - simple induction 1; auto with sets. - - apply d_one. - do 5 intro. - generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)). - simple induction 1. - generalize (app_ass x4 l1 (Cons x2 Nil)); simple induction 1. - intro E. - generalize (app_inj_tail _ _ _ _ E). - simple induction 1; intros. - generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. - rewrite <- H7; rewrite <- H10; generalize H6. - generalize (app_ass x4 l1 (Cons x2 Nil)); intro E1. - rewrite E1. - intro. - generalize (Hind x4 (l1 ++ Cons x2 Nil) H11). - simple induction 1; split. - auto with sets. - - generalize H14. - rewrite <- H10; intro. - apply d_conc; auto with sets. + induction D as [ | |* H D Hind]; intros. + - assert (H0 : x ++ y = Nil) by auto with sets. + apply app_eq_nil in H0 as (->,->). + split; apply d_nil. + - assert (E : x0 ++ y = Cons x Nil) by auto with sets. + apply app_eq_unit in E as [(->,->)|(->,->)]. + + split. + apply d_nil. + apply d_one. + + split. + apply d_one. + apply d_nil. + - induction y0 using rev_ind in x0, H0 |- *. + + rewrite <- app_nil_end in H0. + rewrite <- H0. + split. + apply d_conc; auto with sets. + apply d_nil. + + induction y0 using rev_ind in x1, x0, H0 |- *. + * simpl. + split. + apply app_inj_tail in H0 as (<-,_). assumption. + apply d_one. + * rewrite <- 2!app_ass in H0. + apply app_inj_tail in H0 as (H0,<-). + pose proof H0 as H0'. + apply app_inj_tail in H0' as (_,->). + rewrite app_ass in H0. + apply Hind in H0 as []. + split. + assumption. + apply d_conc; auto with sets. Qed. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index a5e710504..99b631905 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -54,17 +54,17 @@ Theorem Z_lt_abs_rec : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z * P (- z)). - cut (Q (Z.abs p)); [ intros H | apply (Z_lt_rec Q); auto with zarith ]. - elim (Zabs_dec p); intro eq; rewrite eq; - elim H; auto with zarith. - intros x H; subst Q. + enough (H:Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). + apply (Z_lt_rec Q); auto with zarith. + subst Q; intros x H. split; apply HP. - rewrite Z.abs_eq; auto; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_eq; auto; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. Theorem Z_lt_abs_induction : @@ -74,16 +74,17 @@ Theorem Z_lt_abs_induction : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. - cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. - elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q; clear Q; intros. + enough (Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). + apply (Z_lt_induction Q); auto with zarith. + subst Q; intros. split; apply HP. - rewrite Z.abs_eq; auto; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_eq; auto; intros. + elim (H (Z.abs m)); intros; auto with zarith. + elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. (** To do case analysis over the sign of [z] *) diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index e5325aa75..043b68dd3 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -212,13 +212,10 @@ Section Z_BRIC_A_BRAC. (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z. Proof. intros. - cut (2 * Z.div2 z < 2 * two_power_nat n)%Z; intros. - omega. - + enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega. rewrite <- two_power_nat_S. destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros. rewrite <- Zeven.Zeven_div2; auto. - generalize (Zeven.Zodd_div2 z Hodd); omega. Qed. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 32993b2c0..f7843ea74 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -666,17 +666,15 @@ Theorem Zdiv_eucl_extended : {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}. Proof. intros b Hb a. - elim (Z_le_gt_dec 0 b); intro Hb'. - cut (b > 0); [ intro Hb'' | omega ]. - rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. - cut (- b > 0); [ intro Hb'' | omega ]. - elim (Zdiv_eucl_exist Hb'' a); intros qr. - elim qr; intros q r Hqr. - exists (- q, r). - elim Hqr; intros. - split. - rewrite <- Z.mul_opp_comm; assumption. - rewrite Z.abs_neq; [ assumption | omega ]. + destruct (Z_le_gt_dec 0 b) as [Hb'|Hb']. + - assert (Hb'' : b > 0) by omega. + rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. + - assert (Hb'' : - b > 0) by omega. + destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]). + exists (- q, r). + split. + + rewrite <- Z.mul_opp_comm; assumption. + + rewrite Z.abs_neq; [ assumption | omega ]. Qed. Arguments Zdiv_eucl_extended : default implicits. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index aeddeb70c..fa059313f 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -105,8 +105,7 @@ Open Scope Z_scope. Lemma fibonacci_pos : forall n, 0 <= fibonacci n. Proof. - cut (forall N n, (n<N)%nat -> 0<=fibonacci n). - eauto. + enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. induction N. inversion 1. intros. |