diff options
45 files changed, 834 insertions, 797 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 36b9cf06b9..2d34412908 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -31,7 +31,7 @@ Lemma ind_0_1_SS : Proof. intros P H0 H1 H2. fix ind_0_1_SS 1. - destruct n as [|[|n]]. + intros n; destruct n as [|[|n]]. - exact H0. - exact H1. - apply H2, ind_0_1_SS. @@ -105,17 +105,17 @@ Hint Resolve double_S: arith. Lemma even_odd_double n : (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). Proof. - revert n. fix even_odd_double 1. destruct n as [|[|n]]. + revert n. fix even_odd_double 1. intros n; destruct n as [|[|n]]. - (* n = 0 *) split; split; auto with arith. inversion 1. - (* n = 1 *) - split; split; auto with arith. inversion_clear 1. inversion H0. + split; split; auto with arith. inversion_clear 1 as [|? H0]. inversion H0. - (* n = (S (S n')) *) destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')). split; split; simpl div2; rewrite ?double_S. - + inversion_clear 1. inversion_clear H0. auto. + + inversion_clear 1 as [|? H0]. inversion_clear H0. auto. + injection 1. auto with arith. - + inversion_clear 1. inversion_clear H0. auto. + + inversion_clear 1 as [? H0]. inversion_clear H0. auto. + injection 1. auto with arith. Qed. diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index fdd149e01a..d5f715d843 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -21,7 +21,7 @@ Inductive diveucl a b : Set := Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n. Proof. - induction m as (m,H0) using gt_wf_rec. + intros n H m; induction m as (m,H0) using gt_wf_rec. destruct (le_gt_dec n m) as [Hlebn|Hgtbn]. destruct (H0 (m - n)) as (q,r,Hge0,Heq); auto with arith. apply divex with (S q) r; trivial. @@ -34,7 +34,7 @@ Lemma quotient : n > 0 -> forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}. Proof. - induction m as (m,H0) using gt_wf_rec. + intros n H m; induction m as (m,H0) using gt_wf_rec. destruct (le_gt_dec n m) as [Hlebn|Hgtbn]. destruct (H0 (m - n)) as (q & Hq); auto with arith; exists (S q). destruct Hq as (r & Heq & Hgt); exists r; split; trivial. @@ -47,7 +47,7 @@ Lemma modulo : n > 0 -> forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}. Proof. - induction m as (m,H0) using gt_wf_rec. + intros n H m; induction m as (m,H0) using gt_wf_rec. destruct (le_gt_dec n m) as [Hlebn|Hgtbn]. destruct (H0 (m - n)) as (r & Hr); auto with arith; exists r. destruct Hr as (q & Heq & Hgt); exists (S q); split; trivial. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 9c0a6bd96f..3422596818 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -39,28 +39,28 @@ Hint Constructors odd: arith. Lemma even_equiv : forall n, even n <-> Nat.Even n. Proof. fix even_equiv 1. - destruct n as [|[|n]]; simpl. + intros n; destruct n as [|[|n]]; simpl. - split; [now exists 0 | constructor]. - split. - + inversion_clear 1. inversion_clear H0. + + inversion_clear 1 as [|? H0]. inversion_clear H0. + now rewrite <- Nat.even_spec. - rewrite Nat.Even_succ_succ, <- even_equiv. split. - + inversion_clear 1. now inversion_clear H0. + + inversion_clear 1 as [|? H0]. now inversion_clear H0. + now do 2 constructor. Qed. Lemma odd_equiv : forall n, odd n <-> Nat.Odd n. Proof. fix odd_equiv 1. - destruct n as [|[|n]]; simpl. + intros n; destruct n as [|[|n]]; simpl. - split. + inversion_clear 1. + now rewrite <- Nat.odd_spec. - split; [ now exists 0 | do 2 constructor ]. - rewrite Nat.Odd_succ_succ, <- odd_equiv. split. - + inversion_clear 1. now inversion_clear H0. + + inversion_clear 1 as [? H0]. now inversion_clear H0. + now do 2 constructor. Qed. @@ -68,14 +68,14 @@ Qed. Lemma even_or_odd n : even n \/ odd n. Proof. - induction n. + induction n as [|n IHn]. - auto with arith. - elim IHn; auto with arith. Qed. Lemma even_odd_dec n : {even n} + {odd n}. Proof. - induction n. + induction n as [|n IHn]. - auto with arith. - elim IHn; auto with arith. Defined. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index bea14480f8..52605a4667 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -16,7 +16,7 @@ (** A boolean is either [true] or [false], and this is decidable *) Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}. - destruct b; auto. + intros b; destruct b; auto. Defined. Hint Resolve sumbool_of_bool: bool. @@ -24,13 +24,13 @@ Hint Resolve sumbool_of_bool: bool. Definition bool_eq_rec : forall (b:bool) (P:bool -> Set), (b = true -> P true) -> (b = false -> P false) -> P b. - destruct b; auto. + intros b; destruct b; auto. Defined. Definition bool_eq_ind : forall (b:bool) (P:bool -> Prop), (b = true -> P true) -> (b = false -> P false) -> P b. - destruct b; auto. + intros b; destruct b; auto. Defined. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 8280b7d01f..adeb527c1c 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -36,13 +36,13 @@ Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing). Lemma Ptestbit_Pbit : forall p n, Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n. Proof. - induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial; + intro p; induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial; rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite Nat2N.inj_pred. Qed. Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = N.testbit_nat a n. Proof. - destruct a. trivial. apply Ptestbit_Pbit. + intro a; destruct a. trivial. apply Ptestbit_Pbit. Qed. Lemma Pbit_Ptestbit : @@ -54,7 +54,7 @@ Qed. Lemma Nbit_Ntestbit : forall a n, N.testbit_nat a (N.to_nat n) = N.testbit a n. Proof. - destruct a. trivial. apply Pbit_Ptestbit. + intro a; destruct a. trivial. apply Pbit_Ptestbit. Qed. (** Equivalence of shifts, index in [N] or [nat] *) @@ -104,7 +104,7 @@ Qed. Lemma Nshiftr_nat_spec : forall a n m, N.testbit_nat (N.shiftr_nat a n) m = N.testbit_nat a (m+n). Proof. - induction n; intros m. + intros a n; induction n as [|n IHn]; intros m. now rewrite <- plus_n_O. simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn. destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial. @@ -113,7 +113,7 @@ Qed. Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat -> N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n). Proof. - induction n; intros m H. + intros a n; induction n as [|n IHn]; intros m H. - now rewrite Nat.sub_0_r. - destruct m. + inversion H. @@ -125,9 +125,9 @@ Qed. Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat -> N.testbit_nat (N.shiftl_nat a n) m = false. Proof. - induction n; intros m H. inversion H. + intros a n; induction n as [|n IHn]; intros m H. inversion H. rewrite Nshiftl_nat_S. - destruct m. + destruct m as [|m]. - destruct (N.shiftl_nat a n); trivial. - apply Lt.lt_S_n in H. specialize (IHn m H). @@ -147,13 +147,13 @@ Lemma Pshiftl_nat_N : forall p n, Npos (Pos.shiftl_nat p n) = N.shiftl_nat (Npos p) n. Proof. unfold Pos.shiftl_nat, N.shiftl_nat. - induction n; simpl; auto. now rewrite <- IHn. + intros p n; induction n as [|n IHn]; simpl; auto. now rewrite <- IHn. Qed. Lemma Pshiftl_nat_plus : forall n m p, Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m. Proof. - induction m; simpl; intros. reflexivity. + intros n m; induction m; simpl; intros. reflexivity. now f_equal. Qed. @@ -221,13 +221,13 @@ Local Notation Step H := (fun n => H (S n)). Lemma Pbit_faithful_0 : forall p, ~(Pos.testbit_nat p == (fun _ => false)). Proof. - induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O). + intros p; induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O). apply (IHp (Step H)). Qed. Lemma Pbit_faithful : forall p p', Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'. Proof. - induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial; + intros p; induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial; try discriminate (H O). f_equal. apply (IHp _ (Step H)). destruct (Pbit_faithful_0 _ (Step H)). @@ -260,25 +260,25 @@ Definition Neven (n:N) := N.odd n = false. Lemma Nbit0_correct : forall n:N, N.testbit_nat n 0 = N.odd n. Proof. - destruct n; trivial. + intros n; destruct n as [|p]; trivial. destruct p; trivial. Qed. Lemma Ndouble_bit0 : forall n:N, N.odd (N.double n) = false. Proof. - destruct n; trivial. + intros n; destruct n; trivial. Qed. Lemma Ndouble_plus_one_bit0 : forall n:N, N.odd (N.succ_double n) = true. Proof. - destruct n; trivial. + intros n; destruct n; trivial. Qed. Lemma Ndiv2_double : forall n:N, Neven n -> N.double (N.div2 n) = n. Proof. - destruct n. trivial. destruct p. intro H. discriminate H. + intros n; destruct n as [|p]. trivial. destruct p. intro H. discriminate H. intros. reflexivity. intro H. discriminate H. Qed. @@ -286,7 +286,7 @@ Qed. Lemma Ndiv2_double_plus_one : forall n:N, Nodd n -> N.succ_double (N.div2 n) = n. Proof. - destruct n. intro. discriminate H. + intros n; destruct n as [|p]. intro H. discriminate H. destruct p. intros. reflexivity. intro H. discriminate H. intro. reflexivity. @@ -295,21 +295,21 @@ Qed. Lemma Ndiv2_correct : forall (a:N) (n:nat), N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n). Proof. - destruct a; trivial. + intros a; destruct a as [|p]; trivial. destruct p; trivial. Qed. Lemma Nxor_bit0 : forall a a':N, N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a'). Proof. - intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O). + intros a a'. rewrite <- Nbit0_correct, (Nxor_semantics a a' O). rewrite Nbit0_correct, Nbit0_correct. reflexivity. Qed. Lemma Nxor_div2 : forall a a':N, N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a'). Proof. - intros. apply Nbit_faithful. unfold eqf. intro. + intros a a'. apply Nbit_faithful. unfold eqf. intro n. rewrite (Nxor_semantics (N.div2 a) (N.div2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)). rewrite 2! Ndiv2_correct. reflexivity. @@ -319,7 +319,7 @@ Lemma Nneg_bit0 : forall a a':N, N.odd (N.lxor a a') = true -> N.odd a = negb (N.odd a'). Proof. - intros. + intros a a' H. rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. reflexivity. @@ -328,21 +328,21 @@ Qed. Lemma Nneg_bit0_1 : forall a a':N, N.lxor a a' = Npos 1 -> N.odd a = negb (N.odd a'). Proof. - intros. apply Nneg_bit0. rewrite H. reflexivity. + intros a a' H. apply Nneg_bit0. rewrite H. reflexivity. Qed. Lemma Nneg_bit0_2 : forall (a a':N) (p:positive), N.lxor a a' = Npos (xI p) -> N.odd a = negb (N.odd a'). Proof. - intros. apply Nneg_bit0. rewrite H. reflexivity. + intros a a' p H. apply Nneg_bit0. rewrite H. reflexivity. Qed. Lemma Nsame_bit0 : forall (a a':N) (p:positive), N.lxor a a' = Npos (xO p) -> N.odd a = N.odd a'. Proof. - intros. rewrite <- (xorb_false (N.odd a)). + intros a a' p H. rewrite <- (xorb_false (N.odd a)). assert (H0: N.odd (Npos (xO p)) = false) by reflexivity. rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity. @@ -366,7 +366,7 @@ Lemma Nbit0_less : forall a a', N.odd a = false -> N.odd a' = true -> Nless a a' = true. Proof. - intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless. + intros a a' H H0. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless. rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity. assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1. @@ -379,7 +379,7 @@ Lemma Nbit0_gt : forall a a', N.odd a = true -> N.odd a' = false -> Nless a a' = false. Proof. - intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless. + intros a a' H H0. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless. rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity. assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1. @@ -390,13 +390,13 @@ Qed. Lemma Nless_not_refl : forall a, Nless a a = false. Proof. - intro. unfold Nless. rewrite (N.lxor_nilpotent a). reflexivity. + intro a. unfold Nless. rewrite (N.lxor_nilpotent a). reflexivity. Qed. Lemma Nless_def_1 : forall a a', Nless (N.double a) (N.double a') = Nless a a'. Proof. - destruct a; destruct a'. reflexivity. + intros a a'; destruct a as [|p]; destruct a' as [|p0]. reflexivity. trivial. unfold Nless. simpl. destruct p; trivial. unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity. @@ -407,7 +407,7 @@ Lemma Nless_def_2 : forall a a', Nless (N.succ_double a) (N.succ_double a') = Nless a a'. Proof. - destruct a; destruct a'. reflexivity. + intros a a'; destruct a as [|p]; destruct a' as [|p0]. reflexivity. trivial. unfold Nless. simpl. destruct p; trivial. unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity. @@ -430,20 +430,20 @@ Qed. Lemma Nless_z : forall a, Nless a N0 = false. Proof. - induction a. reflexivity. + intros a; induction a as [|p]. reflexivity. unfold Nless. rewrite (N.lxor_0_r (Npos p)). induction p; trivial. Qed. Lemma N0_less_1 : forall a, Nless N0 a = true -> {p : positive | a = Npos p}. Proof. - destruct a. discriminate. + intros a; destruct a as [|p]. discriminate. intros. exists p. reflexivity. Qed. Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0. Proof. - induction a as [|p]; intro H. trivial. + intros a; induction a as [|p]; intro H. trivial. exfalso. induction p as [|p IHp|]; discriminate || simpl; auto using IHp. Qed. @@ -451,14 +451,14 @@ Lemma Nless_trans : forall a a' a'', Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true. Proof. - induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0. + intros a; induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0. - case_eq (Nless N0 a'') ; intros Heqn. + trivial. + rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0. - induction a' as [|a' _|a' _] using N.binary_ind. + rewrite (Nless_z (N.double a)) in H. discriminate H. + rewrite (Nless_def_1 a a') in H. - induction a'' using N.binary_ind. + induction a'' as [|a'' _|a'' _] using N.binary_ind. * rewrite (Nless_z (N.double a')) in H0. discriminate H0. * rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a''). exact (IHa _ _ H H0). @@ -470,7 +470,7 @@ Proof. - induction a' as [|a' _|a' _] using N.binary_ind. + rewrite (Nless_z (N.succ_double a)) in H. discriminate H. + rewrite (Nless_def_4 a a') in H. discriminate H. - + induction a'' using N.binary_ind. + + induction a'' as [|a'' _|a'' _] using N.binary_ind. * rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. * rewrite (Nless_def_4 a' a'') in H0. discriminate H0. * rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H. @@ -480,7 +480,7 @@ Qed. Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. - induction a using N.binary_rec; intro a'. + intro a; induction a as [|a IHa|a IHa] using N.binary_rec; intro a'. - case_eq (Nless N0 a') ; intros Heqb. + left. left. auto. + right. rewrite (N0_less_2 a' Heqb). reflexivity. @@ -553,9 +553,9 @@ Definition ByteV2N {n : nat} : ByteVector n -> N := Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. Proof. -destruct n. +intro n; destruct n as [|p]. simpl; auto. -induction p; simpl in *; auto; rewrite IHp; simpl; auto. +induction p as [p IHp|p IHp|]; simpl in *; auto; rewrite IHp; simpl; auto. Qed. (** The opposite composition is not so simple: if the considered @@ -564,7 +564,7 @@ Qed. Lemma Bv2N_Nsize : forall n (bv:Bvector n), N.size_nat (Bv2N n bv) <= n. Proof. -induction bv; intros. +intros n bv; induction bv as [|h n bv]; intros. auto. simpl. destruct h; @@ -579,16 +579,16 @@ Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), Bsign _ bv = true <-> N.size_nat (Bv2N _ bv) = (S n). Proof. -apply Vector.rectS ; intros ; simpl. +apply Vector.rectS ; intros a ; simpl. destruct a ; compute ; split ; intros x ; now inversion x. - destruct a, (Bv2N (S n) v) ; + intros n v IH; destruct a, (Bv2N (S n) v) ; simpl ;intuition ; try discriminate. Qed. Lemma Bv2N_upper_bound (n : nat) (bv : Bvector n) : (Bv2N bv < N.shiftl_nat 1 n)%N. Proof with simpl; auto. - induction bv... + induction bv as [|h]... - constructor. - destruct h. + apply N.succ_double_lt... @@ -621,7 +621,7 @@ Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (N.size_nat a) a. Proof. -destruct a; simpl. +intro a; destruct a as [|p]; simpl. auto. induction p; simpl; intros; auto; congruence. Qed. @@ -632,7 +632,7 @@ Qed. Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), N2Bv_gen (N.size_nat a + k) a = Vector.append (N2Bv a) (Bvect_false k). Proof. -destruct a; simpl. +intros a k; destruct a as [|p]; simpl. destruct k; simpl; auto. induction p; simpl; intros;unfold Bcons; f_equal; auto. Qed. @@ -642,7 +642,7 @@ Qed. Lemma N2Bv_Bv2N : forall n (bv:Bvector n), N2Bv_gen n (Bv2N n bv) = bv. Proof. -induction bv; intros. +intros n bv; induction bv as [|h n bv IHbv]; intros. auto. simpl. generalize IHbv; clear IHbv. @@ -658,7 +658,7 @@ Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), N.odd (Bv2N _ bv) = Blow _ bv. Proof. apply Vector.caseS. -intros. +intros h n t. unfold Blow. simpl. destruct (Bv2N n t); simpl; @@ -670,9 +670,9 @@ Notation Bnth := (@Vector.nth_order bool). Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), Bnth bv H = N.testbit_nat (Bv2N _ bv) p. Proof. -induction bv; intros. +intros n bv; induction bv as [|h n bv IHbv]; intros p H. inversion H. -destruct p ; simpl. +destruct p as [|p]; simpl. destruct (Bv2N n bv); destruct h; simpl in *; auto. specialize IHbv with p (Lt.lt_S_n _ _ H). simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto. @@ -680,9 +680,9 @@ Qed. Lemma Nbit_Nsize : forall n p, N.size_nat n <= p -> N.testbit_nat n p = false. Proof. -destruct n as [|n]. +intro n; destruct n as [|n]. simpl; auto. -induction n; simpl in *; intros; destruct p; auto with arith. +induction n; simpl in *; intros p H; destruct p; auto with arith. inversion H. inversion H. Qed. @@ -690,9 +690,9 @@ Qed. Lemma Nbit_Bth: forall n p (H:p < N.size_nat n), N.testbit_nat n p = Bnth (N2Bv n) H. Proof. -destruct n as [|n]. -inversion H. -induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto. +intro n; destruct n as [|n]. +intros p H; inversion H. +induction n ; intro p; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto. intros H ; destruct (Lt.lt_n_O _ (Lt.lt_S_n _ _ H)). Qed. @@ -701,8 +701,9 @@ Qed. Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), Bv2N _ (BVxor _ bv bv') = N.lxor (Bv2N _ bv) (Bv2N _ bv'). Proof. -apply Vector.rect2 ; intros. +apply Vector.rect2. now simpl. +intros n v1 v2 H a b. simpl. destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl in *; rewrite H ; now simpl. Qed. @@ -710,8 +711,8 @@ Qed. Lemma Nand_BVand : forall n (bv bv' : Bvector n), Bv2N _ (BVand _ bv bv') = N.land (Bv2N _ bv) (Bv2N _ bv'). Proof. -refine (@Vector.rect2 _ _ _ _ _); simpl; intros; auto. -rewrite H. +refine (@Vector.rect2 _ _ _ _ _); simpl; auto. +intros n v1 v2 H a b; rewrite H. destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl; auto. Qed. @@ -719,15 +720,15 @@ Qed. Lemma N2Bv_sized_Nsize (n : N) : N2Bv_sized (N.size_nat n) n = N2Bv n. Proof with simpl; auto. - destruct n... - induction p... + destruct n as [|p]... + induction p as [p IHp|p IHp|]... all: rewrite IHp... Qed. Lemma N2Bv_sized_Bv2N (n : nat) (v : Bvector n) : N2Bv_sized n (Bv2N n v) = v. Proof with simpl; auto. - induction v... + induction v as [|h n v IHv]... destruct h; unfold N2Bv_sized; destruct (Bv2N n v) as [|[]]; @@ -737,6 +738,6 @@ Qed. Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) : N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k. Proof with auto. - destruct a... + destruct a as [|p]... induction p; simpl; f_equal... Qed. diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 2361d59c26..0c097b6773 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -20,159 +20,157 @@ Include ZBaseProp Z. Hint Rewrite opp_0 : nz. -Theorem add_pred_l : forall n m, P n + m == P (n + m). +Theorem add_pred_l n m : P n + m == P (n + m). Proof. -intros n m. rewrite <- (succ_pred n) at 2. now rewrite add_succ_l, pred_succ. Qed. -Theorem add_pred_r : forall n m, n + P m == P (n + m). +Theorem add_pred_r n m : n + P m == P (n + m). Proof. -intros n m; rewrite 2 (add_comm n); apply add_pred_l. +rewrite 2 (add_comm n); apply add_pred_l. Qed. -Theorem add_opp_r : forall n m, n + (- m) == n - m. +Theorem add_opp_r n m : n + (- m) == n - m. Proof. nzinduct m. now nzsimpl. intro m. rewrite opp_succ, sub_succ_r, add_pred_r. now rewrite pred_inj_wd. Qed. -Theorem sub_0_l : forall n, 0 - n == - n. +Theorem sub_0_l n : 0 - n == - n. Proof. -intro n; rewrite <- add_opp_r; now rewrite add_0_l. +rewrite <- add_opp_r; now rewrite add_0_l. Qed. -Theorem sub_succ_l : forall n m, S n - m == S (n - m). +Theorem sub_succ_l n m : S n - m == S (n - m). Proof. -intros n m; rewrite <- 2 add_opp_r; now rewrite add_succ_l. +rewrite <- 2 add_opp_r; now rewrite add_succ_l. Qed. -Theorem sub_pred_l : forall n m, P n - m == P (n - m). +Theorem sub_pred_l n m : P n - m == P (n - m). Proof. -intros n m. rewrite <- (succ_pred n) at 2. +rewrite <- (succ_pred n) at 2. rewrite sub_succ_l; now rewrite pred_succ. Qed. -Theorem sub_pred_r : forall n m, n - (P m) == S (n - m). +Theorem sub_pred_r n m : n - (P m) == S (n - m). Proof. -intros n m. rewrite <- (succ_pred m) at 2. +rewrite <- (succ_pred m) at 2. rewrite sub_succ_r; now rewrite succ_pred. Qed. -Theorem opp_pred : forall n, - (P n) == S (- n). +Theorem opp_pred n : - (P n) == S (- n). Proof. -intro n. rewrite <- (succ_pred n) at 2. +rewrite <- (succ_pred n) at 2. rewrite opp_succ. now rewrite succ_pred. Qed. -Theorem sub_diag : forall n, n - n == 0. +Theorem sub_diag n : n - n == 0. Proof. nzinduct n. now nzsimpl. intro n. rewrite sub_succ_r, sub_succ_l; now rewrite pred_succ. Qed. -Theorem add_opp_diag_l : forall n, - n + n == 0. +Theorem add_opp_diag_l n : - n + n == 0. Proof. -intro n; now rewrite add_comm, add_opp_r, sub_diag. +now rewrite add_comm, add_opp_r, sub_diag. Qed. -Theorem add_opp_diag_r : forall n, n + (- n) == 0. +Theorem add_opp_diag_r n : n + (- n) == 0. Proof. -intro n; rewrite add_comm; apply add_opp_diag_l. +rewrite add_comm; apply add_opp_diag_l. Qed. -Theorem add_opp_l : forall n m, - m + n == n - m. +Theorem add_opp_l n m : - m + n == n - m. Proof. -intros n m; rewrite <- add_opp_r; now rewrite add_comm. +rewrite <- add_opp_r; now rewrite add_comm. Qed. -Theorem add_sub_assoc : forall n m p, n + (m - p) == (n + m) - p. +Theorem add_sub_assoc n m p : n + (m - p) == (n + m) - p. Proof. -intros n m p; rewrite <- 2 add_opp_r; now rewrite add_assoc. +rewrite <- 2 add_opp_r; now rewrite add_assoc. Qed. -Theorem opp_involutive : forall n, - (- n) == n. +Theorem opp_involutive n : - (- n) == n. Proof. nzinduct n. now nzsimpl. intro n. rewrite opp_succ, opp_pred. now rewrite succ_inj_wd. Qed. -Theorem opp_add_distr : forall n m, - (n + m) == - n + (- m). +Theorem opp_add_distr n m : - (n + m) == - n + (- m). Proof. -intros n m; nzinduct n. +nzinduct n. now nzsimpl. intro n. rewrite add_succ_l; do 2 rewrite opp_succ; rewrite add_pred_l. now rewrite pred_inj_wd. Qed. -Theorem opp_sub_distr : forall n m, - (n - m) == - n + m. +Theorem opp_sub_distr n m : - (n - m) == - n + m. Proof. -intros n m; rewrite <- add_opp_r, opp_add_distr. +rewrite <- add_opp_r, opp_add_distr. now rewrite opp_involutive. Qed. -Theorem opp_inj : forall n m, - n == - m -> n == m. +Theorem opp_inj n m : - n == - m -> n == m. Proof. -intros n m H. apply opp_wd in H. now rewrite 2 opp_involutive in H. +intros H. apply opp_wd in H. now rewrite 2 opp_involutive in H. Qed. -Theorem opp_inj_wd : forall n m, - n == - m <-> n == m. +Theorem opp_inj_wd n m : - n == - m <-> n == m. Proof. -intros n m; split; [apply opp_inj | intros; now f_equiv]. +split; [apply opp_inj | intros; now f_equiv]. Qed. -Theorem eq_opp_l : forall n m, - n == m <-> n == - m. +Theorem eq_opp_l n m : - n == m <-> n == - m. Proof. -intros n m. now rewrite <- (opp_inj_wd (- n) m), opp_involutive. +now rewrite <- (opp_inj_wd (- n) m), opp_involutive. Qed. -Theorem eq_opp_r : forall n m, n == - m <-> - n == m. +Theorem eq_opp_r n m : n == - m <-> - n == m. Proof. symmetry; apply eq_opp_l. Qed. -Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p. +Theorem sub_add_distr n m p : n - (m + p) == (n - m) - p. Proof. -intros n m p; rewrite <- add_opp_r, opp_add_distr, add_assoc. +rewrite <- add_opp_r, opp_add_distr, add_assoc. now rewrite 2 add_opp_r. Qed. -Theorem sub_sub_distr : forall n m p, n - (m - p) == (n - m) + p. +Theorem sub_sub_distr n m p : n - (m - p) == (n - m) + p. Proof. -intros n m p; rewrite <- add_opp_r, opp_sub_distr, add_assoc. +rewrite <- add_opp_r, opp_sub_distr, add_assoc. now rewrite add_opp_r. Qed. -Theorem sub_opp_l : forall n m, - n - m == - m - n. +Theorem sub_opp_l n m : - n - m == - m - n. Proof. -intros n m. rewrite <- 2 add_opp_r. now rewrite add_comm. +rewrite <- 2 add_opp_r. now rewrite add_comm. Qed. -Theorem sub_opp_r : forall n m, n - (- m) == n + m. +Theorem sub_opp_r n m : n - (- m) == n + m. Proof. -intros n m; rewrite <- add_opp_r; now rewrite opp_involutive. +rewrite <- add_opp_r; now rewrite opp_involutive. Qed. -Theorem add_sub_swap : forall n m p, n + m - p == n - p + m. +Theorem add_sub_swap n m p : n + m - p == n - p + m. Proof. -intros n m p. rewrite <- add_sub_assoc, <- (add_opp_r n p), <- add_assoc. +rewrite <- add_sub_assoc, <- (add_opp_r n p), <- add_assoc. now rewrite add_opp_l. Qed. -Theorem sub_cancel_l : forall n m p, n - m == n - p <-> m == p. +Theorem sub_cancel_l n m p : n - m == n - p <-> m == p. Proof. -intros n m p. rewrite <- (add_cancel_l (n - m) (n - p) (- n)). +rewrite <- (add_cancel_l (n - m) (n - p) (- n)). rewrite 2 add_sub_assoc. rewrite add_opp_diag_l; rewrite 2 sub_0_l. apply opp_inj_wd. Qed. -Theorem sub_cancel_r : forall n m p, n - p == m - p <-> n == m. +Theorem sub_cancel_r n m p : n - p == m - p <-> n == m. Proof. -intros n m p. stepl (n - p + p == m - p + p) by apply add_cancel_r. now do 2 rewrite <- sub_sub_distr, sub_diag, sub_0_r. Qed. @@ -182,16 +180,15 @@ Qed. in the original equation ([add] or [sub]) and the indication whether the left or right term is moved. *) -Theorem add_move_l : forall n m p, n + m == p <-> m == p - n. +Theorem add_move_l n m p : n + m == p <-> m == p - n. Proof. -intros n m p. stepl (n + m - n == p - n) by apply sub_cancel_r. now rewrite add_comm, <- add_sub_assoc, sub_diag, add_0_r. Qed. -Theorem add_move_r : forall n m p, n + m == p <-> n == p - m. +Theorem add_move_r n m p : n + m == p <-> n == p - m. Proof. -intros n m p; rewrite add_comm; now apply add_move_l. +rewrite add_comm; now apply add_move_l. Qed. (** The two theorems above do not allow rewriting subformulas of the @@ -199,98 +196,98 @@ Qed. right-hand side of the equation. Hence the following two theorems. *) -Theorem sub_move_l : forall n m p, n - m == p <-> - m == p - n. +Theorem sub_move_l n m p : n - m == p <-> - m == p - n. Proof. -intros n m p; rewrite <- (add_opp_r n m); apply add_move_l. +rewrite <- (add_opp_r n m); apply add_move_l. Qed. -Theorem sub_move_r : forall n m p, n - m == p <-> n == p + m. +Theorem sub_move_r n m p : n - m == p <-> n == p + m. Proof. -intros n m p; rewrite <- (add_opp_r n m). now rewrite add_move_r, sub_opp_r. +rewrite <- (add_opp_r n m). now rewrite add_move_r, sub_opp_r. Qed. -Theorem add_move_0_l : forall n m, n + m == 0 <-> m == - n. +Theorem add_move_0_l n m : n + m == 0 <-> m == - n. Proof. -intros n m; now rewrite add_move_l, sub_0_l. +now rewrite add_move_l, sub_0_l. Qed. -Theorem add_move_0_r : forall n m, n + m == 0 <-> n == - m. +Theorem add_move_0_r n m : n + m == 0 <-> n == - m. Proof. -intros n m; now rewrite add_move_r, sub_0_l. +now rewrite add_move_r, sub_0_l. Qed. -Theorem sub_move_0_l : forall n m, n - m == 0 <-> - m == - n. +Theorem sub_move_0_l n m : n - m == 0 <-> - m == - n. Proof. -intros n m. now rewrite sub_move_l, sub_0_l. +now rewrite sub_move_l, sub_0_l. Qed. -Theorem sub_move_0_r : forall n m, n - m == 0 <-> n == m. +Theorem sub_move_0_r n m : n - m == 0 <-> n == m. Proof. -intros n m. now rewrite sub_move_r, add_0_l. +now rewrite sub_move_r, add_0_l. Qed. (** The following section is devoted to cancellation of like terms. The name includes the first operator and the position of the term being canceled. *) -Theorem add_simpl_l : forall n m, n + m - n == m. +Theorem add_simpl_l n m : n + m - n == m. Proof. -intros; now rewrite add_sub_swap, sub_diag, add_0_l. +now rewrite add_sub_swap, sub_diag, add_0_l. Qed. -Theorem add_simpl_r : forall n m, n + m - m == n. +Theorem add_simpl_r n m : n + m - m == n. Proof. -intros; now rewrite <- add_sub_assoc, sub_diag, add_0_r. +now rewrite <- add_sub_assoc, sub_diag, add_0_r. Qed. -Theorem sub_simpl_l : forall n m, - n - m + n == - m. +Theorem sub_simpl_l n m : - n - m + n == - m. Proof. -intros; now rewrite <- add_sub_swap, add_opp_diag_l, sub_0_l. +now rewrite <- add_sub_swap, add_opp_diag_l, sub_0_l. Qed. -Theorem sub_simpl_r : forall n m, n - m + m == n. +Theorem sub_simpl_r n m : n - m + m == n. Proof. -intros; now rewrite <- sub_sub_distr, sub_diag, sub_0_r. +now rewrite <- sub_sub_distr, sub_diag, sub_0_r. Qed. -Theorem sub_add : forall n m, m - n + n == m. +Theorem sub_add n m : m - n + n == m. Proof. - intros. now rewrite <- add_sub_swap, add_simpl_r. +now rewrite <- add_sub_swap, add_simpl_r. Qed. (** Now we have two sums or differences; the name includes the two operators and the position of the terms being canceled *) -Theorem add_add_simpl_l_l : forall n m p, (n + m) - (n + p) == m - p. +Theorem add_add_simpl_l_l n m p : (n + m) - (n + p) == m - p. Proof. -intros n m p. now rewrite (add_comm n m), <- add_sub_assoc, +now rewrite (add_comm n m), <- add_sub_assoc, sub_add_distr, sub_diag, sub_0_l, add_opp_r. Qed. -Theorem add_add_simpl_l_r : forall n m p, (n + m) - (p + n) == m - p. +Theorem add_add_simpl_l_r n m p : (n + m) - (p + n) == m - p. Proof. -intros n m p. rewrite (add_comm p n); apply add_add_simpl_l_l. +rewrite (add_comm p n); apply add_add_simpl_l_l. Qed. -Theorem add_add_simpl_r_l : forall n m p, (n + m) - (m + p) == n - p. +Theorem add_add_simpl_r_l n m p : (n + m) - (m + p) == n - p. Proof. -intros n m p. rewrite (add_comm n m); apply add_add_simpl_l_l. +rewrite (add_comm n m); apply add_add_simpl_l_l. Qed. -Theorem add_add_simpl_r_r : forall n m p, (n + m) - (p + m) == n - p. +Theorem add_add_simpl_r_r n m p : (n + m) - (p + m) == n - p. Proof. -intros n m p. rewrite (add_comm p m); apply add_add_simpl_r_l. +rewrite (add_comm p m); apply add_add_simpl_r_l. Qed. -Theorem sub_add_simpl_r_l : forall n m p, (n - m) + (m + p) == n + p. +Theorem sub_add_simpl_r_l n m p : (n - m) + (m + p) == n + p. Proof. -intros n m p. now rewrite <- sub_sub_distr, sub_add_distr, sub_diag, +now rewrite <- sub_sub_distr, sub_add_distr, sub_diag, sub_0_l, sub_opp_r. Qed. -Theorem sub_add_simpl_r_r : forall n m p, (n - m) + (p + m) == n + p. +Theorem sub_add_simpl_r_r n m p : (n - m) + (p + m) == n + p. Proof. -intros n m p. rewrite (add_comm p m); apply sub_add_simpl_r_l. +rewrite (add_comm p m); apply sub_add_simpl_r_l. Qed. (** Of course, there are many other variants *) diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 40a37be5f9..5a293c6483 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -241,25 +241,25 @@ Qed. Theorem sub_neg_cases : forall n m, n - m < 0 -> n < 0 \/ 0 < m. Proof. -intros. +intros n m ?. rewrite <- (opp_neg_pos m). apply add_neg_cases. now rewrite add_opp_r. Qed. Theorem sub_pos_cases : forall n m, 0 < n - m -> 0 < n \/ m < 0. Proof. -intros. +intros n m ?. rewrite <- (opp_pos_neg m). apply add_pos_cases. now rewrite add_opp_r. Qed. Theorem sub_nonpos_cases : forall n m, n - m <= 0 -> n <= 0 \/ 0 <= m. Proof. -intros. +intros n m ?. rewrite <- (opp_nonpos_nonneg m). apply add_nonpos_cases. now rewrite add_opp_r. Qed. Theorem sub_nonneg_cases : forall n m, 0 <= n - m -> 0 <= n \/ m <= 0. Proof. -intros. +intros n m ?. rewrite <- (opp_nonneg_nonpos m). apply add_nonneg_cases. now rewrite add_opp_r. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 0f40d3d7b6..4d2361689d 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -244,7 +244,7 @@ Qed. Lemma bit0_odd : forall a, a.[0] = odd a. Proof. - intros. symmetry. + intros a. symmetry. destruct (exists_div2 a) as (a' & b & EQ). rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2. destruct b; simpl; apply odd_1 || apply odd_0. @@ -428,14 +428,14 @@ Qed. Lemma mul_pow2_bits : forall a n m, 0<=n -> (a*2^n).[m] = a.[m-n]. Proof. - intros. + intros a n m ?. rewrite <- (add_simpl_r m n) at 1. rewrite add_sub_swap, add_comm. now apply mul_pow2_bits_add. Qed. Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false. Proof. - intros. + intros a n m ?. destruct (le_gt_cases 0 n). rewrite mul_pow2_bits by trivial. apply testbit_neg_r. now apply lt_sub_0. @@ -561,7 +561,10 @@ Proof. split. apply bits_inj'. intros EQ n Hn; now rewrite EQ. Qed. -Ltac bitwise := apply bits_inj'; intros ?m ?Hm; autorewrite with bitwise. +Tactic Notation "bitwise" "as" simple_intropattern(m) simple_intropattern(Hm) + := apply bits_inj'; intros m Hm; autorewrite with bitwise. + +Ltac bitwise := bitwise as ?m ?Hm. Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. @@ -619,7 +622,7 @@ Qed. Lemma shiftl_spec : forall a n m, 0<=m -> (a << n).[m] = a.[m-n]. Proof. - intros. + intros a n m ?. destruct (le_gt_cases n m). now apply shiftl_spec_high. rewrite shiftl_spec_low, testbit_neg_r; trivial. now apply lt_sub_0. @@ -693,7 +696,7 @@ Qed. Lemma shiftl_shiftl : forall a n m, 0<=n -> (a << n) << m == a << (n+m). Proof. - intros a n p Hn. bitwise. + intros a n p Hn. bitwise as m Hm. rewrite 2 (shiftl_spec _ _ m) by trivial. rewrite add_comm, sub_add_distr. destruct (le_gt_cases 0 (m-p)) as [H|H]. @@ -745,8 +748,8 @@ Qed. Lemma shiftl_0_l : forall n, 0 << n == 0. Proof. - intros. - destruct (le_ge_cases 0 n). + intros n. + destruct (le_ge_cases 0 n) as [H|H]. rewrite shiftl_mul_pow2 by trivial. now nzsimpl. rewrite shiftl_div_pow2 by trivial. rewrite <- opp_nonneg_nonpos in H. nzsimpl; order_nz. @@ -901,7 +904,7 @@ Qed. Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0. Proof. - intros a b H. bitwise. + intros a b H. bitwise as m ?. apply (orb_false_iff a.[m] b.[m]). now rewrite <- lor_spec, H, bits_0. Qed. @@ -909,7 +912,7 @@ Qed. Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0. Proof. intros a b. split. - split. now apply lor_eq_0_l in H. + intro H; split. now apply lor_eq_0_l in H. rewrite lor_comm in H. now apply lor_eq_0_l in H. intros (EQ,EQ'). now rewrite EQ, lor_0_l. Qed. @@ -1022,13 +1025,13 @@ Proof. unfold clearbit. solve_proper. Qed. Lemma pow2_bits_true : forall n, 0<=n -> (2^n).[n] = true. Proof. - intros. rewrite <- (mul_1_l (2^n)). + intros n ?. rewrite <- (mul_1_l (2^n)). now rewrite mul_pow2_bits, sub_diag, bit0_odd, odd_1. Qed. Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false. Proof. - intros. + intros n m ?. destruct (le_gt_cases 0 n); [|now rewrite pow_neg_r, bits_0]. destruct (le_gt_cases n m). rewrite <- (mul_1_l (2^n)), mul_pow2_bits; trivial. @@ -1073,7 +1076,7 @@ Qed. Lemma clearbit_eqb : forall a n m, (clearbit a n).[m] = a.[m] && negb (eqb n m). Proof. - intros. + intros a n m. destruct (le_gt_cases 0 m); [| now rewrite 2 testbit_neg_r]. rewrite clearbit_spec', ldiff_spec. f_equal. f_equal. destruct (le_gt_cases 0 n) as [Hn|Hn]. @@ -1090,7 +1093,7 @@ Qed. Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false. Proof. - intros. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). + intros a n. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). apply andb_false_r. Qed. @@ -1161,7 +1164,7 @@ Proof. unfold lnot. solve_proper. Qed. Lemma lnot_spec : forall a n, 0<=n -> (lnot a).[n] = negb a.[n]. Proof. - intros. unfold lnot. rewrite <- (opp_involutive a) at 2. + intros a n ?. unfold lnot. rewrite <- (opp_involutive a) at 2. rewrite bits_opp, negb_involutive; trivial. Qed. @@ -1214,7 +1217,7 @@ Qed. Lemma lor_lnot_diag : forall a, lor a (lnot a) == -1. Proof. - intros a. bitwise. rewrite lnot_spec, bits_m1; trivial. + intros a. bitwise as m ?. rewrite lnot_spec, bits_m1; trivial. now destruct a.[m]. Qed. @@ -1267,7 +1270,7 @@ Qed. Lemma lxor_m1_r : forall a, lxor a (-1) == lnot a. Proof. - intros. now rewrite <- (lxor_0_r (lnot a)), <- lnot_m1, lxor_lnot_lnot. + intros a. now rewrite <- (lxor_0_r (lnot a)), <- lnot_m1, lxor_lnot_lnot. Qed. Lemma lxor_m1_l : forall a, lxor (-1) a == lnot a. @@ -1278,7 +1281,7 @@ Qed. Lemma lxor_lor : forall a b, land a b == 0 -> lxor a b == lor a b. Proof. - intros a b H. bitwise. + intros a b H. bitwise as m ?. assert (a.[m] && b.[m] = false) by now rewrite <- land_spec, H, bits_0. now destruct a.[m], b.[m]. @@ -1299,7 +1302,7 @@ Proof. unfold ones. solve_proper. Qed. Lemma ones_equiv : forall n, ones n == P (2^n). Proof. - intros. unfold ones. + intros n. unfold ones. destruct (le_gt_cases 0 n). now rewrite shiftl_mul_pow2, mul_1_l. f_equiv. rewrite pow_neg_r; trivial. @@ -1367,7 +1370,7 @@ Qed. Lemma lor_ones_low : forall a n, 0<=a -> log2 a < n -> lor a (ones n) == ones n. Proof. - intros a n Ha H. bitwise. destruct (le_gt_cases n m). + intros a n Ha H. bitwise as m ?. destruct (le_gt_cases n m). rewrite ones_spec_high, bits_above_log2; try split; trivial. now apply lt_le_trans with n. apply le_trans with (log2 a); order_pos. @@ -1376,7 +1379,7 @@ Qed. Lemma land_ones : forall a n, 0<=n -> land a (ones n) == a mod 2^n. Proof. - intros a n Hn. bitwise. destruct (le_gt_cases n m). + intros a n Hn. bitwise as m ?. destruct (le_gt_cases n m). rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r; try split; trivial. rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r; @@ -1396,7 +1399,7 @@ Qed. Lemma ldiff_ones_r : forall a n, 0<=n -> ldiff a (ones n) == (a >> n) << n. Proof. - intros a n Hn. bitwise. destruct (le_gt_cases n m). + intros a n Hn. bitwise as m ?. destruct (le_gt_cases n m). rewrite ones_spec_high, shiftl_spec_high, shiftr_spec; trivial. rewrite sub_add; trivial. apply andb_true_r. now apply le_0_sub. @@ -1408,7 +1411,7 @@ Qed. Lemma ldiff_ones_r_low : forall a n, 0<=a -> log2 a < n -> ldiff a (ones n) == 0. Proof. - intros a n Ha H. bitwise. destruct (le_gt_cases n m). + intros a n Ha H. bitwise as m ?. destruct (le_gt_cases n m). rewrite ones_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. split; trivial. now apply le_trans with (log2 a); order_pos. @@ -1418,7 +1421,7 @@ Qed. Lemma ldiff_ones_l_low : forall a n, 0<=a -> log2 a < n -> ldiff (ones n) a == lxor a (ones n). Proof. - intros a n Ha H. bitwise. destruct (le_gt_cases n m). + intros a n Ha H. bitwise as m ?. destruct (le_gt_cases n m). rewrite ones_spec_high, bits_above_log2; trivial. now apply lt_le_trans with n. split; trivial. now apply le_trans with (log2 a); order_pos. @@ -1585,7 +1588,7 @@ Qed. Lemma log2_shiftr : forall a n, 0<a -> log2 (a >> n) == max 0 (log2 a - n). Proof. intros a n Ha. - destruct (le_gt_cases 0 (log2 a - n)); + destruct (le_gt_cases 0 (log2 a - n)) as [H|H]; [rewrite max_r | rewrite max_l]; try order. apply log2_bits_unique. now rewrite shiftr_spec, sub_add, bit_log2. @@ -1698,7 +1701,7 @@ Qed. Lemma add_carry_div2 : forall a b (c0:bool), (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0. Proof. - intros. + intros a b c0. rewrite <- add3_bits_div2. rewrite (add_comm ((a/2)+_)). rewrite <- div_add by order'. @@ -1767,7 +1770,7 @@ Proof. apply div_lt_upper_bound. order'. now rewrite <- pow_succ_r. exists (c0 + 2*c). repeat split. (* step, add *) - bitwise. + bitwise as m Hm. le_elim Hm. rewrite <- (succ_pred m), lt_succ_r in Hm. rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial. @@ -1777,7 +1780,7 @@ Proof. now rewrite add_b2z_double_bit0, add3_bit0, b2z_bit0. (* step, carry *) rewrite add_b2z_double_div2. - bitwise. + bitwise as m Hm. le_elim Hm. rewrite <- (succ_pred m), lt_succ_r in Hm. rewrite <- (succ_pred m), <- !div2_bits, IH2 by trivial. @@ -1905,7 +1908,7 @@ Proof. rewrite sub_add. symmetry. rewrite add_nocarry_lxor; trivial. - bitwise. + bitwise as m ?. apply bits_inj_iff in H. specialize (H m). rewrite ldiff_spec, bits_0 in H. now destruct a.[m], b.[m]. @@ -1938,7 +1941,7 @@ Lemma add_nocarry_mod_lt_pow2 : forall a b n, 0<=n -> land a b == 0 -> Proof. intros a b n Hn H. apply add_nocarry_lt_pow2. - bitwise. + bitwise as m ?. destruct (le_gt_cases n m). rewrite mod_pow2_bits_high; now split. now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 44cba37eb2..d28d010ae8 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -51,7 +51,7 @@ Qed. Lemma mod_bound_abs : forall a b, b~=0 -> abs (a mod b) < abs b. Proof. -intros. +intros a b **. destruct (abs_spec b) as [(LE,EQ)|(LE,EQ)]; rewrite EQ. destruct (mod_pos_bound a b). order. now rewrite abs_eq. destruct (mod_neg_bound a b). order. rewrite abs_neq; trivial. @@ -87,11 +87,11 @@ Qed. Theorem div_unique_pos: forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b. -Proof. intros; apply div_unique with r; auto. Qed. +Proof. intros a b q r **; apply div_unique with r; auto. Qed. Theorem div_unique_neg: forall a b q r, b<r<=0 -> a == b*q + r -> q == a/b. -Proof. intros; apply div_unique with r; auto. Qed. +Proof. intros a b q r **; apply div_unique with r; auto. Qed. Theorem mod_unique: forall a b q r, (0<=r<b \/ b<r<=0) -> a == b*q + r -> r == a mod b. @@ -106,11 +106,11 @@ Qed. Theorem mod_unique_pos: forall a b q r, 0<=r<b -> a == b*q + r -> r == a mod b. -Proof. intros; apply mod_unique with q; auto. Qed. +Proof. intros a b q r **; apply mod_unique with q; auto. Qed. Theorem mod_unique_neg: forall a b q r, b<r<=0 -> a == b*q + r -> r == a mod b. -Proof. intros; apply mod_unique with q; auto. Qed. +Proof. intros a b q r **; apply mod_unique with q; auto. Qed. (** Sign rules *) @@ -121,7 +121,7 @@ Ltac pos_or_neg a := Fact mod_bound_or : forall a b, b~=0 -> 0<=a mod b<b \/ b<a mod b<=0. Proof. -intros. +intros a b **. destruct (lt_ge_cases 0 b); [left|right]. apply mod_pos_bound; trivial. apply mod_neg_bound; order. Qed. @@ -129,7 +129,7 @@ Qed. Fact opp_mod_bound_or : forall a b, b~=0 -> 0 <= -(a mod b) < -b \/ -b < -(a mod b) <= 0. Proof. -intros. +intros a b **. destruct (lt_ge_cases 0 b); [right|left]. rewrite <- opp_lt_mono, opp_nonpos_nonneg. destruct (mod_pos_bound a b); intuition; order. @@ -139,14 +139,14 @@ Qed. Lemma div_opp_opp : forall a b, b~=0 -> -a/-b == a/b. Proof. -intros. symmetry. apply div_unique with (- (a mod b)). +intros a b **. symmetry. apply div_unique with (- (a mod b)). now apply opp_mod_bound_or. rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order. Qed. Lemma mod_opp_opp : forall a b, b~=0 -> (-a) mod (-b) == - (a mod b). Proof. -intros. symmetry. apply mod_unique with (a/b). +intros a b **. symmetry. apply mod_unique with (a/b). now apply opp_mod_bound_or. rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order. Qed. @@ -200,28 +200,28 @@ Qed. Lemma div_opp_r_z : forall a b, b~=0 -> a mod b == 0 -> a/(-b) == -(a/b). Proof. -intros. rewrite <- (opp_involutive a) at 1. +intros a b **. rewrite <- (opp_involutive a) at 1. rewrite div_opp_opp; auto using div_opp_l_z. Qed. Lemma div_opp_r_nz : forall a b, b~=0 -> a mod b ~= 0 -> a/(-b) == -(a/b)-1. Proof. -intros. rewrite <- (opp_involutive a) at 1. +intros a b **. rewrite <- (opp_involutive a) at 1. rewrite div_opp_opp; auto using div_opp_l_nz. Qed. Lemma mod_opp_r_z : forall a b, b~=0 -> a mod b == 0 -> a mod (-b) == 0. Proof. -intros. rewrite <- (opp_involutive a) at 1. +intros a b **. rewrite <- (opp_involutive a) at 1. now rewrite mod_opp_opp, mod_opp_l_z, opp_0. Qed. Lemma mod_opp_r_nz : forall a b, b~=0 -> a mod b ~= 0 -> a mod (-b) == (a mod b) - b. Proof. -intros. rewrite <- (opp_involutive a) at 1. +intros a b **. rewrite <- (opp_involutive a) at 1. rewrite mod_opp_opp, mod_opp_l_nz by trivial. now rewrite opp_sub_distr, add_comm, add_opp_r. Qed. @@ -247,7 +247,7 @@ Qed. Lemma mod_sign_mul : forall a b, b~=0 -> 0 <= (a mod b) * b. Proof. -intros. destruct (lt_ge_cases 0 b). +intros a b **. destruct (lt_ge_cases 0 b). apply mul_nonneg_nonneg; destruct (mod_pos_bound a b); order. apply mul_nonpos_nonpos; destruct (mod_neg_bound a b); order. Qed. @@ -256,7 +256,7 @@ Qed. Lemma div_same : forall a, a~=0 -> a/a == 1. Proof. -intros. pos_or_neg a. apply div_same; order. +intros a ?. pos_or_neg a. apply div_same; order. rewrite <- div_opp_opp by trivial. now apply div_same. Qed. @@ -279,7 +279,7 @@ Proof. exact mod_small. Qed. Lemma div_0_l: forall a, a~=0 -> 0/a == 0. Proof. -intros. pos_or_neg a. apply div_0_l; order. +intros a ?. pos_or_neg a. apply div_0_l; order. rewrite <- div_opp_opp, opp_0 by trivial. now apply div_0_l. Qed. @@ -308,7 +308,7 @@ Proof. exact mod_1_l. Qed. Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a. Proof. -intros. symmetry. apply div_unique with 0. +intros a b ?. symmetry. apply div_unique with 0. destruct (lt_ge_cases 0 b); [left|right]; split; order. nzsimpl; apply mul_comm. Qed. @@ -350,7 +350,7 @@ Qed. Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> 0<=a<b \/ b<a<=0). Proof. -intros. +intros a b **. rewrite <- div_small_iff, mod_eq by trivial. rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l. rewrite eq_sym_iff, eq_mul_0. tauto. @@ -393,7 +393,7 @@ Qed. Lemma mul_div_le : forall a b, 0<b -> b*(a/b) <= a. Proof. -intros. +intros a b **. rewrite (div_mod a b) at 2; try order. rewrite <- (add_0_r (b*(a/b))) at 1. rewrite <- add_le_mono_l. @@ -412,7 +412,7 @@ Qed. Lemma mul_succ_div_gt: forall a b, 0<b -> a < b*(S (a/b)). Proof. -intros. +intros a b ?. nzsimpl. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. @@ -432,7 +432,7 @@ Qed. Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0). Proof. -intros. +intros a b **. rewrite (div_mod a b) at 1; try order. rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. @@ -443,7 +443,7 @@ Qed. Theorem div_lt_upper_bound: forall a b q, 0<b -> a < b*q -> a/b < q. Proof. -intros. +intros a b q **. rewrite (mul_lt_mono_pos_l b) by trivial. apply le_lt_trans with a; trivial. now apply mul_div_le. @@ -452,7 +452,7 @@ Qed. Theorem div_le_upper_bound: forall a b q, 0<b -> a <= b*q -> a/b <= q. Proof. -intros. +intros a b q **. rewrite <- (div_mul q b) by order. apply div_le_mono; trivial. now rewrite mul_comm. Qed. @@ -460,7 +460,7 @@ Qed. Theorem div_le_lower_bound: forall a b q, 0<b -> b*q <= a -> q <= a/b. Proof. -intros. +intros a b q **. rewrite <- (div_mul q b) by order. apply div_le_mono; trivial. now rewrite mul_comm. Qed. @@ -475,7 +475,7 @@ Proof. exact div_le_compat_l. Qed. Lemma mod_add : forall a b c, c~=0 -> (a + b * c) mod c == a mod c. Proof. -intros. +intros a b c **. symmetry. apply mod_unique with (a/c+b); trivial. now apply mod_bound_or. @@ -486,7 +486,7 @@ Qed. Lemma div_add : forall a b c, c~=0 -> (a + b * c) / c == a / c + b. Proof. -intros. +intros a b c **. apply (mul_cancel_l _ _ c); try order. apply (add_cancel_r _ _ ((a+b*c) mod c)). rewrite <- div_mod, mod_add by order. @@ -506,7 +506,7 @@ Qed. Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> (a*c)/(b*c) == a/b. Proof. -intros. +intros a b c **. symmetry. apply div_unique with ((a mod b)*c). (* ineqs *) @@ -525,13 +525,13 @@ Qed. Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 -> (c*a)/(c*b) == a/b. Proof. -intros. rewrite !(mul_comm c); now apply div_mul_cancel_r. +intros a b c **. rewrite !(mul_comm c); now apply div_mul_cancel_r. Qed. Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 -> (c*a) mod (c*b) == c * (a mod b). Proof. -intros. +intros a b c **. rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))). rewrite <- div_mod. rewrite div_mul_cancel_l by trivial. @@ -543,7 +543,7 @@ Qed. Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 -> (a*c) mod (b*c) == (a mod b) * c. Proof. - intros. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. + intros a b c **. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. Qed. @@ -570,7 +570,7 @@ Qed. Lemma mul_mod_idemp_r : forall a b n, n~=0 -> (a*(b mod n)) mod n == (a*b) mod n. Proof. - intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l. + intros a b n **. rewrite !(mul_comm a). now apply mul_mod_idemp_l. Qed. Theorem mul_mod: forall a b n, n~=0 -> @@ -591,7 +591,7 @@ Qed. Lemma add_mod_idemp_r : forall a b n, n~=0 -> (a+(b mod n)) mod n == (a+b) mod n. Proof. - intros. rewrite !(add_comm a). now apply add_mod_idemp_l. + intros a b n **. rewrite !(add_comm a). now apply add_mod_idemp_l. Qed. Theorem add_mod: forall a b n, n~=0 -> diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 4915d69c5b..7d374bd4be 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -69,7 +69,7 @@ Proof. intros. now rewrite rem_opp_r, rem_opp_l. Qed. Lemma quot_opp_l : forall a b, b ~= 0 -> (-a)÷b == -(a÷b). Proof. -intros. +intros a b ?. rewrite <- (mul_cancel_l _ _ b) by trivial. rewrite <- (add_cancel_r _ _ ((-a) rem b)). now rewrite <- quot_rem, rem_opp_l, mul_opp_r, <- opp_add_distr, <- quot_rem. @@ -77,7 +77,7 @@ Qed. Lemma quot_opp_r : forall a b, b ~= 0 -> a÷(-b) == -(a÷b). Proof. -intros. +intros a b ?. assert (-b ~= 0) by (now rewrite eq_opp_l, opp_0). rewrite <- (mul_cancel_l _ _ (-b)) by trivial. rewrite <- (add_cancel_r _ _ (a rem (-b))). @@ -105,17 +105,17 @@ Qed. Theorem quot_unique: forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a÷b. -Proof. intros; now apply NZQuot.div_unique with r. Qed. +Proof. intros a b q r **; now apply NZQuot.div_unique with r. Qed. Theorem rem_unique: forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a rem b. -Proof. intros; now apply NZQuot.mod_unique with q. Qed. +Proof. intros a b q r **; now apply NZQuot.mod_unique with q. Qed. (** A division by itself returns 1 *) Lemma quot_same : forall a, a~=0 -> a÷a == 1. Proof. -intros. pos_or_neg a. apply NZQuot.div_same; order. +intros a ?. pos_or_neg a. apply NZQuot.div_same; order. rewrite <- quot_opp_opp by trivial. now apply NZQuot.div_same. Qed. @@ -138,7 +138,7 @@ Proof. exact NZQuot.mod_small. Qed. Lemma quot_0_l: forall a, a~=0 -> 0÷a == 0. Proof. -intros. pos_or_neg a. apply NZQuot.div_0_l; order. +intros a ?. pos_or_neg a. apply NZQuot.div_0_l; order. rewrite <- quot_opp_opp, opp_0 by trivial. now apply NZQuot.div_0_l. Qed. @@ -149,7 +149,7 @@ Qed. Lemma quot_1_r: forall a, a÷1 == a. Proof. -intros. pos_or_neg a. now apply NZQuot.div_1_r. +intros a. pos_or_neg a. now apply NZQuot.div_1_r. apply opp_inj. rewrite <- quot_opp_l. apply NZQuot.div_1_r; order. intro EQ; symmetry in EQ; revert EQ; apply lt_neq, lt_0_1. Qed. @@ -168,7 +168,7 @@ Proof. exact NZQuot.mod_1_l. Qed. Lemma quot_mul : forall a b, b~=0 -> (a*b)÷b == a. Proof. -intros. pos_or_neg a; pos_or_neg b. apply NZQuot.div_mul; order. +intros a b ?. pos_or_neg a; pos_or_neg b. apply NZQuot.div_mul; order. rewrite <- quot_opp_opp, <- mul_opp_r by order. apply NZQuot.div_mul; order. rewrite <- opp_inj_wd, <- quot_opp_l, <- mul_opp_l by order. apply NZQuot.div_mul; order. @@ -190,7 +190,7 @@ Qed. Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b. Proof. - intros. pos_or_neg b. destruct (rem_bound_pos a b); order. + intros a b **. pos_or_neg b. destruct (rem_bound_pos a b); order. rewrite <- rem_opp_r; trivial. destruct (rem_bound_pos a (-b)); trivial. Qed. @@ -309,7 +309,7 @@ Proof. exact NZQuot.div_str_pos. Qed. Lemma quot_small_iff : forall a b, b~=0 -> (a÷b==0 <-> abs a < abs b). Proof. -intros. pos_or_neg a; pos_or_neg b. +intros a b ?. pos_or_neg a; pos_or_neg b. rewrite NZQuot.div_small_iff; try order. rewrite 2 abs_eq; intuition; order. rewrite <- opp_inj_wd, opp_0, <- quot_opp_r, NZQuot.div_small_iff by order. rewrite (abs_eq a), (abs_neq' b); intuition; order. @@ -321,7 +321,7 @@ Qed. Lemma rem_small_iff : forall a b, b~=0 -> (a rem b == a <-> abs a < abs b). Proof. -intros. rewrite rem_eq, <- quot_small_iff by order. +intros a b ?. rewrite rem_eq, <- quot_small_iff by order. rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l. rewrite eq_sym_iff, eq_mul_0. tauto. Qed. @@ -336,7 +336,7 @@ Proof. exact NZQuot.div_lt. Qed. Lemma quot_le_mono : forall a b c, 0<c -> a<=b -> a÷c <= b÷c. Proof. -intros. pos_or_neg a. apply NZQuot.div_le_mono; auto. +intros a b c **. pos_or_neg a. apply NZQuot.div_le_mono; auto. pos_or_neg b. apply le_trans with 0. rewrite <- opp_nonneg_nonpos, <- quot_opp_l by order. apply quot_pos; order. @@ -350,7 +350,7 @@ Qed. Lemma mul_quot_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a÷b) <= a. Proof. -intros. pos_or_neg b. +intros a b **. pos_or_neg b. split. apply mul_nonneg_nonneg; [|apply quot_pos]; order. apply NZQuot.mul_div_le; order. @@ -362,7 +362,7 @@ Qed. Lemma mul_quot_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a÷b) <= 0. Proof. -intros. +intros a b **. rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-quot_opp_l by order. rewrite <- opp_nonneg_nonpos in *. destruct (mul_quot_le (-a) b); tauto. @@ -415,7 +415,7 @@ Proof. exact NZQuot.div_lt_upper_bound. Qed. Theorem quot_le_upper_bound: forall a b q, 0<b -> a <= b*q -> a÷b <= q. Proof. -intros. +intros a b q **. rewrite <- (quot_mul q b) by order. apply quot_le_mono; trivial. now rewrite mul_comm. Qed. @@ -423,7 +423,7 @@ Qed. Theorem quot_le_lower_bound: forall a b q, 0<b -> b*q <= a -> q <= a÷b. Proof. -intros. +intros a b q **. rewrite <- (quot_mul q b) by order. apply quot_le_mono; trivial. now rewrite mul_comm. Qed. @@ -443,7 +443,7 @@ Lemma rem_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> (a + b * c) rem c == a rem c. Proof. assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) rem c == a rem c). - intros. pos_or_neg c. apply NZQuot.mod_add; order. + intros a b c **. pos_or_neg c. apply NZQuot.mod_add; order. rewrite <- (rem_opp_r a), <- (rem_opp_r (a+b*c)) by order. rewrite <- mul_opp_opp in *. apply NZQuot.mod_add; order. @@ -457,7 +457,7 @@ Qed. Lemma quot_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> (a + b * c) ÷ c == a ÷ c + b. Proof. -intros. +intros a b c **. rewrite <- (mul_cancel_l _ _ c) by trivial. rewrite <- (add_cancel_r _ _ ((a+b*c) rem c)). rewrite <- quot_rem, rem_add by trivial. @@ -476,14 +476,14 @@ Lemma quot_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> (a*c)÷(b*c) == a÷b. Proof. assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)÷(b*c) == a÷b). - intros. pos_or_neg c. apply NZQuot.div_mul_cancel_r; order. + intros a b c **. pos_or_neg c. apply NZQuot.div_mul_cancel_r; order. rewrite <- quot_opp_opp, <- 2 mul_opp_r. apply NZQuot.div_mul_cancel_r; order. rewrite <- neq_mul_0; intuition order. assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)÷(b*c) == a÷b). - intros. pos_or_neg b. apply Aux1; order. + intros a b c **. pos_or_neg b. apply Aux1; order. apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_l; try order. apply Aux1; order. rewrite <- neq_mul_0; intuition order. -intros. pos_or_neg a. apply Aux2; order. +intros a b c **. pos_or_neg a. apply Aux2; order. apply opp_inj. rewrite <- 2 quot_opp_l, <- mul_opp_l; try order. apply Aux2; order. rewrite <- neq_mul_0; intuition order. Qed. @@ -491,13 +491,13 @@ Qed. Lemma quot_mul_cancel_l : forall a b c, b~=0 -> c~=0 -> (c*a)÷(c*b) == a÷b. Proof. -intros. rewrite !(mul_comm c); now apply quot_mul_cancel_r. +intros a b c **. rewrite !(mul_comm c); now apply quot_mul_cancel_r. Qed. Lemma mul_rem_distr_r: forall a b c, b~=0 -> c~=0 -> (a*c) rem (b*c) == (a rem b) * c. Proof. -intros. +intros a b c **. assert (b*c ~= 0) by (rewrite <- neq_mul_0; tauto). rewrite ! rem_eq by trivial. rewrite quot_mul_cancel_r by order. @@ -507,7 +507,7 @@ Qed. Lemma mul_rem_distr_l: forall a b c, b~=0 -> c~=0 -> (c*a) rem (c*b) == c * (a rem b). Proof. -intros; rewrite !(mul_comm c); now apply mul_rem_distr_r. +intros a b c **; rewrite !(mul_comm c); now apply mul_rem_distr_r. Qed. (** Operations modulo. *) @@ -515,7 +515,7 @@ Qed. Theorem rem_rem: forall a n, n~=0 -> (a rem n) rem n == a rem n. Proof. -intros. pos_or_neg a; pos_or_neg n. apply NZQuot.mod_mod; order. +intros a n **. pos_or_neg a; pos_or_neg n. apply NZQuot.mod_mod; order. rewrite <- ! (rem_opp_r _ n) by trivial. apply NZQuot.mod_mod; order. apply opp_inj. rewrite <- !rem_opp_l by order. apply NZQuot.mod_mod; order. apply opp_inj. rewrite <- !rem_opp_opp by order. apply NZQuot.mod_mod; order. @@ -526,11 +526,11 @@ Lemma mul_rem_idemp_l : forall a b n, n~=0 -> Proof. assert (Aux1 : forall a b n, 0<=a -> 0<=b -> n~=0 -> ((a rem n)*b) rem n == (a*b) rem n). - intros. pos_or_neg n. apply NZQuot.mul_mod_idemp_l; order. + intros a b n **. pos_or_neg n. apply NZQuot.mul_mod_idemp_l; order. rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.mul_mod_idemp_l; order. assert (Aux2 : forall a b n, 0<=a -> n~=0 -> ((a rem n)*b) rem n == (a*b) rem n). - intros. pos_or_neg b. now apply Aux1. + intros a b n **. pos_or_neg b. now apply Aux1. apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_r by order. apply Aux1; order. intros a b n Hn. pos_or_neg a. now apply Aux2. @@ -541,7 +541,7 @@ Qed. Lemma mul_rem_idemp_r : forall a b n, n~=0 -> (a*(b rem n)) rem n == (a*b) rem n. Proof. -intros. rewrite !(mul_comm a). now apply mul_rem_idemp_l. +intros a b n **. rewrite !(mul_comm a). now apply mul_rem_idemp_l. Qed. Theorem mul_rem: forall a b n, n~=0 -> @@ -564,7 +564,7 @@ Lemma add_rem_idemp_l : forall a b n, n~=0 -> 0 <= a*b -> Proof. assert (Aux : forall a b n, 0<=a -> 0<=b -> n~=0 -> ((a rem n)+b) rem n == (a+b) rem n). - intros. pos_or_neg n. apply NZQuot.add_mod_idemp_l; order. + intros a b n **. pos_or_neg n. apply NZQuot.add_mod_idemp_l; order. rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.add_mod_idemp_l; order. intros a b n Hn Hab. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]. now apply Aux. @@ -576,7 +576,7 @@ Qed. Lemma add_rem_idemp_r : forall a b n, n~=0 -> 0 <= a*b -> (a+(b rem n)) rem n == (a+b) rem n. Proof. -intros. rewrite !(add_comm a). apply add_rem_idemp_l; trivial. +intros a b n **. rewrite !(add_comm a). apply add_rem_idemp_l; trivial. now rewrite mul_comm. Qed. @@ -598,16 +598,16 @@ Lemma quot_quot : forall a b c, b~=0 -> c~=0 -> (a÷b)÷c == a÷(b*c). Proof. assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a÷b)÷c == a÷(b*c)). - intros. pos_or_neg c. apply NZQuot.div_div; order. + intros a b c **. pos_or_neg c. apply NZQuot.div_div; order. apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_r; trivial. apply NZQuot.div_div; order. rewrite <- neq_mul_0; intuition order. assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a÷b)÷c == a÷(b*c)). - intros. pos_or_neg b. apply Aux1; order. + intros a b c **. pos_or_neg b. apply Aux1; order. apply opp_inj. rewrite <- quot_opp_l, <- 2 quot_opp_r, <- mul_opp_l; trivial. apply Aux1; trivial. rewrite <- neq_mul_0; intuition order. -intros. pos_or_neg a. apply Aux2; order. +intros a b c **. pos_or_neg a. apply Aux2; order. apply opp_inj. rewrite <- 3 quot_opp_l; try order. apply Aux2; order. rewrite <- neq_mul_0. tauto. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index 09d28a18ec..755557ff17 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -98,7 +98,7 @@ Qed. Lemma gcd_abs_l : forall n m, gcd (abs n) m == gcd n m. Proof. - intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. easy. apply gcd_opp_l. Qed. @@ -125,7 +125,7 @@ Qed. Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m. Proof. - intros. apply gcd_unique_alt; try apply gcd_nonneg. + intros n m p. apply gcd_unique_alt; try apply gcd_nonneg. intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial. apply divide_add_r; trivial. now apply divide_mul_r. apply divide_add_cancel_r with (p*n); trivial. @@ -164,12 +164,12 @@ Proof. (* First, a version restricted to natural numbers *) 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. + apply (fun H => strong_right_induction _ H 0); trivial. 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. + apply (fun H => strong_right_induction _ H 0); trivial. unfold Bezout. solve_proper. clear m Hm. intros m Hm IHm. destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. @@ -227,7 +227,7 @@ Qed. Lemma gcd_mul_mono_l_nonneg : forall n m p, 0<=p -> gcd (p*n) (p*m) == p * gcd n m. Proof. - intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_l. + intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_l. Qed. Lemma gcd_mul_mono_r : @@ -239,7 +239,7 @@ Qed. Lemma gcd_mul_mono_r_nonneg : forall n m p, 0<=p -> gcd (n*p) (m*p) == gcd n m * p. Proof. - intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r. + intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r. Qed. Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p). diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index 6aa828ebfc..c45ea12868 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -33,14 +33,14 @@ Module Type ZLcmProp Lemma quot_div_nonneg : forall a b, 0<=a -> 0<b -> a÷b == a/b. Proof. - intros. apply div_unique_pos with (a rem b). + intros a b **. apply div_unique_pos with (a rem b). now apply rem_bound_pos. apply quot_rem. order. Qed. Lemma rem_mod_nonneg : forall a b, 0<=a -> 0<b -> a rem b == a mod b. Proof. - intros. apply mod_unique_pos with (a÷b). + intros a b **. apply mod_unique_pos with (a÷b). now apply rem_bound_pos. apply quot_rem. order. Qed. @@ -290,7 +290,7 @@ Qed. Lemma lcm_divide_iff : forall n m p, (lcm n m | p) <-> (n | p) /\ (m | p). Proof. - intros. split. split. + intros n m p. split. split. transitivity (lcm n m); trivial using divide_lcm_l. transitivity (lcm n m); trivial using divide_lcm_r. intros (H,H'). now apply lcm_least. @@ -387,7 +387,7 @@ Qed. Lemma lcm_abs_l : forall n m, lcm (abs n) m == lcm n m. Proof. - intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. easy. apply lcm_opp_l. Qed. @@ -438,7 +438,7 @@ Qed. Lemma lcm_mul_mono_l_nonneg : forall n m p, 0<=p -> lcm (p*n) (p*m) == p * lcm n m. Proof. - intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_l. + intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_l. Qed. Lemma lcm_mul_mono_r : @@ -450,7 +450,7 @@ Qed. Lemma lcm_mul_mono_r_nonneg : forall n m p, 0<=p -> lcm (n*p) (m*p) == lcm n m * p. Proof. - intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_r. + intros n m p ?. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_r. Qed. Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 -> diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v index ed0b0c69a0..4af24b7754 100644 --- a/theories/Numbers/Integer/Abstract/ZMaxMin.v +++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v @@ -20,133 +20,133 @@ Include ZMulOrderProp Z. (** Succ *) -Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m). +Lemma succ_max_distr n m : S (max n m) == max (S n) (S m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono. Qed. -Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m). +Lemma succ_min_distr n m : S (min n m) == min (S n) (S m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono. Qed. (** Pred *) -Lemma pred_max_distr : forall n m, P (max n m) == max (P n) (P m). +Lemma pred_max_distr n m : P (max n m) == max (P n) (P m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?pred_le_mono. Qed. -Lemma pred_min_distr : forall n m, P (min n m) == min (P n) (P m). +Lemma pred_min_distr n m : P (min n m) == min (P n) (P m). Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?pred_le_mono. Qed. (** Add *) -Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m. +Lemma add_max_distr_l n m p : max (p + n) (p + m) == p + max n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l. Qed. -Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p. +Lemma add_max_distr_r n m p : max (n + p) (m + p) == max n m + p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r. Qed. -Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m. +Lemma add_min_distr_l n m p : min (p + n) (p + m) == p + min n m. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l. Qed. -Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p. +Lemma add_min_distr_r n m p : min (n + p) (m + p) == min n m + p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r. Qed. (** Opp *) -Lemma opp_max_distr : forall n m, -(max n m) == min (-n) (-m). +Lemma opp_max_distr n m : -(max n m) == min (-n) (-m). Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite max_r by trivial. symmetry. apply min_r. now rewrite <- opp_le_mono. rewrite max_l by trivial. symmetry. apply min_l. now rewrite <- opp_le_mono. Qed. -Lemma opp_min_distr : forall n m, -(min n m) == max (-n) (-m). +Lemma opp_min_distr n m : -(min n m) == max (-n) (-m). Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite min_l by trivial. symmetry. apply max_l. now rewrite <- opp_le_mono. rewrite min_r by trivial. symmetry. apply max_r. now rewrite <- opp_le_mono. Qed. (** Sub *) -Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m. +Lemma sub_max_distr_l n m p : max (p - n) (p - m) == p - min n m. Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite min_l by trivial. apply max_l. now rewrite <- sub_le_mono_l. rewrite min_r by trivial. apply max_r. now rewrite <- sub_le_mono_l. Qed. -Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p. +Lemma sub_max_distr_r n m p : max (n - p) (m - p) == max n m - p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r. Qed. -Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m. +Lemma sub_min_distr_l n m p : min (p - n) (p - m) == p - max n m. Proof. - intros. destruct (le_ge_cases n m). + destruct (le_ge_cases n m). rewrite max_r by trivial. apply min_r. now rewrite <- sub_le_mono_l. rewrite max_l by trivial. apply min_l. now rewrite <- sub_le_mono_l. Qed. -Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p. +Lemma sub_min_distr_r n m p : min (n - p) (m - p) == min n m - p. Proof. - intros. destruct (le_ge_cases n m); + destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r. Qed. (** Mul *) -Lemma mul_max_distr_nonneg_l : forall n m p, 0 <= p -> +Lemma mul_max_distr_nonneg_l n m p : 0 <= p -> max (p * n) (p * m) == p * max n m. Proof. intros. destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_l. Qed. -Lemma mul_max_distr_nonneg_r : forall n m p, 0 <= p -> +Lemma mul_max_distr_nonneg_r n m p : 0 <= p -> max (n * p) (m * p) == max n m * p. Proof. intros. destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_r. Qed. -Lemma mul_min_distr_nonneg_l : forall n m p, 0 <= p -> +Lemma mul_min_distr_nonneg_l n m p : 0 <= p -> min (p * n) (p * m) == p * min n m. Proof. intros. destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_l. Qed. -Lemma mul_min_distr_nonneg_r : forall n m p, 0 <= p -> +Lemma mul_min_distr_nonneg_r n m p : 0 <= p -> min (n * p) (m * p) == min n m * p. Proof. intros. destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_r. Qed. -Lemma mul_max_distr_nonpos_l : forall n m p, p <= 0 -> +Lemma mul_max_distr_nonpos_l n m p : p <= 0 -> max (p * n) (p * m) == p * min n m. Proof. intros. destruct (le_ge_cases n m). @@ -154,7 +154,7 @@ Proof. rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_l. Qed. -Lemma mul_max_distr_nonpos_r : forall n m p, p <= 0 -> +Lemma mul_max_distr_nonpos_r n m p : p <= 0 -> max (n * p) (m * p) == min n m * p. Proof. intros. destruct (le_ge_cases n m). @@ -162,7 +162,7 @@ Proof. rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_r. Qed. -Lemma mul_min_distr_nonpos_l : forall n m p, p <= 0 -> +Lemma mul_min_distr_nonpos_l n m p : p <= 0 -> min (p * n) (p * m) == p * max n m. Proof. intros. destruct (le_ge_cases n m). @@ -170,7 +170,7 @@ Proof. rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_l. Qed. -Lemma mul_min_distr_nonpos_r : forall n m p, p <= 0 -> +Lemma mul_min_distr_nonpos_r n m p : p <= 0 -> min (n * p) (m * p) == max n m * p. Proof. intros. destruct (le_ge_cases n m). diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 7d97d11818..0275a5fa65 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -167,7 +167,7 @@ Qed. Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1. Proof. assert (F := lt_m1_0). -zero_pos_neg n. +intro n; zero_pos_neg n. (* n = 0 *) intros m. nzsimpl. now left. (* 0 < n, proving P n /\ P (-n) *) @@ -205,7 +205,7 @@ Qed. Theorem lt_mul_r : forall n m p, 0 < n -> 1 < p -> n < m -> n < m * p. Proof. -intros. stepl (n * 1) by now rewrite mul_1_r. +intros n m p **. stepl (n * 1) by now rewrite mul_1_r. apply mul_lt_mono_nonneg. now apply lt_le_incl. assumption. apply le_0_1. assumption. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 4b61b18479..0f68278cf0 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -19,19 +19,19 @@ Include NZParityProp Z Z ZP. Lemma odd_pred : forall n, odd (P n) = even n. Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. + intros n. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. Qed. Lemma even_pred : forall n, even (P n) = odd n. Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. + intros n. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. Qed. Lemma even_opp : forall n, even (-n) = even n. Proof. assert (H : forall n, Even n -> Even (-n)). intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv. - intros. rewrite eq_iff_eq_true, !even_spec. + intros n. rewrite eq_iff_eq_true, !even_spec. split. rewrite <- (opp_involutive n) at 2. apply H. apply H. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index bec77fd136..9557212a86 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -73,7 +73,7 @@ Qed. Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b. Proof. - intros. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ. + intros a b ?. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ. reflexivity. symmetry. now apply pow_opp_even. Qed. @@ -119,7 +119,7 @@ Qed. Lemma abs_pow : forall a b, abs (a^b) == (abs a)^b. Proof. intros a b. - destruct (Even_or_Odd b). + destruct (Even_or_Odd b) as [H|H]. rewrite pow_even_abs by trivial. apply abs_eq, pow_nonneg, abs_nonneg. rewrite pow_odd_abs_sgn by trivial. diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index 03e0c0345d..3ebbec9397 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -40,11 +40,11 @@ Module Type GenericSgn (Import Z : ZDecAxiomsSig') (Import ZP : ZMulOrderProp Z) <: HasSgn Z. Definition sgn n := match compare 0 n with Eq => 0 | Lt => 1 | Gt => -1 end. - Lemma sgn_null : forall n, n==0 -> sgn n == 0. + Lemma sgn_null n : n==0 -> sgn n == 0. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. - Lemma sgn_pos : forall n, 0<n -> sgn n == 1. + Lemma sgn_pos n : 0<n -> sgn n == 1. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. - Lemma sgn_neg : forall n, n<0 -> sgn n == -1. + Lemma sgn_neg n : n<0 -> sgn n == -1. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. End GenericSgn. @@ -101,7 +101,7 @@ Qed. Lemma abs_opp : forall n, abs (-n) == abs n. Proof. - intros. destruct_max n. + intros n. destruct_max n. rewrite (abs_neq (-n)), opp_involutive. reflexivity. now rewrite opp_nonpos_nonneg. rewrite (abs_eq (-n)). reflexivity. @@ -115,14 +115,14 @@ Qed. Lemma abs_0_iff : forall n, abs n == 0 <-> n==0. Proof. - split. destruct_max n; auto. + intros n; split. destruct_max n; auto. now rewrite eq_opp_l, opp_0. intros EQ; rewrite EQ. rewrite abs_eq; auto using eq_refl, le_refl. Qed. Lemma abs_pos : forall n, 0 < abs n <-> n~=0. Proof. - intros. rewrite <- abs_0_iff. split; [intros LT| intros NEQ]. + intros n. rewrite <- abs_0_iff. split; [intros LT| intros NEQ]. intro EQ. rewrite EQ in LT. now elim (lt_irrefl 0). assert (LE : 0 <= abs n) by apply abs_nonneg. rewrite lt_eq_cases in LE; destruct LE; auto. @@ -131,12 +131,12 @@ Qed. Lemma abs_eq_or_opp : forall n, abs n == n \/ abs n == -n. Proof. - intros. destruct_max n; auto with relations. + intros n. destruct_max n; auto with relations. Qed. Lemma abs_or_opp_abs : forall n, n == abs n \/ n == - abs n. Proof. - intros. destruct_max n; rewrite ? opp_involutive; auto with relations. + intros n. destruct_max n; rewrite ? opp_involutive; auto with relations. Qed. Lemma abs_involutive : forall n, abs (abs n) == abs n. @@ -147,7 +147,7 @@ Qed. Lemma abs_spec : forall n, (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n). Proof. - intros. destruct (le_gt_cases 0 n). + intros n. destruct (le_gt_cases 0 n). left; split; auto. now apply abs_eq. right; split; auto. apply abs_neq. now apply lt_le_incl. Qed. @@ -156,7 +156,7 @@ Lemma abs_case_strong : forall (P:t->Prop) n, Proper (eq==>iff) P -> (0<=n -> P n) -> (n<=0 -> P (-n)) -> P (abs n). Proof. - intros. destruct_max n; auto. + intros P n **. destruct_max n; auto. Qed. Lemma abs_case : forall (P:t->Prop) n, Proper (eq==>iff) P -> @@ -196,7 +196,7 @@ Qed. Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m. Proof. - intros. destruct_max n; destruct_max m. + intros n m. destruct_max n; destruct_max m. rewrite abs_eq. apply le_refl. now apply add_nonneg_nonneg. destruct_max (n+m); try rewrite opp_add_distr; apply add_le_mono_l || apply add_le_mono_r. @@ -212,7 +212,7 @@ Qed. Lemma abs_sub_triangle : forall n m, abs n - abs m <= abs (n-m). Proof. - intros. + intros n m. rewrite le_sub_le_add_l, add_comm. rewrite <- (sub_simpl_r n m) at 1. apply abs_triangle. @@ -223,10 +223,10 @@ Qed. Lemma abs_mul : forall n m, abs (n * m) == abs n * abs m. Proof. assert (H : forall n m, 0<=n -> abs (n*m) == n * abs m). - intros. destruct_max m. + intros n m ?. destruct_max m. rewrite abs_eq. apply eq_refl. now apply mul_nonneg_nonneg. rewrite abs_neq, mul_opp_r. reflexivity. now apply mul_nonneg_nonpos . - intros. destruct_max n. now apply H. + intros n m. destruct_max n. now apply H. rewrite <- mul_opp_opp, H, abs_opp. reflexivity. now apply opp_nonneg_nonpos. Qed. @@ -271,7 +271,7 @@ Qed. Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n. Proof. - split; try apply sgn_pos. destruct_sgn n; auto. + intros n; split; try apply sgn_pos. destruct_sgn n; auto. intros. elim (lt_neq 0 1); auto. apply lt_0_1. intros. elim (lt_neq (-1) 1); auto. apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. @@ -279,7 +279,7 @@ Qed. Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0. Proof. - split; try apply sgn_null. destruct_sgn n; auto with relations. + intros n; split; try apply sgn_null. destruct_sgn n; auto with relations. intros. elim (lt_neq 0 1); auto with relations. apply lt_0_1. intros. elim (lt_neq (-1) 0); auto. rewrite opp_neg_pos. apply lt_0_1. @@ -287,7 +287,7 @@ Qed. Lemma sgn_neg_iff : forall n, sgn n == -1 <-> n<0. Proof. - split; try apply sgn_neg. destruct_sgn n; auto with relations. + intros n; split; try apply sgn_neg. destruct_sgn n; auto with relations. intros. elim (lt_neq (-1) 1); auto with relations. apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. intros. elim (lt_neq (-1) 0); auto with relations. @@ -296,7 +296,7 @@ Qed. Lemma sgn_opp : forall n, sgn (-n) == - sgn n. Proof. - intros. destruct_sgn n. + intros n. destruct_sgn n. apply sgn_neg. now rewrite opp_neg_pos. setoid_replace n with 0 by auto with relations. rewrite opp_0. apply sgn_0. @@ -305,7 +305,7 @@ Qed. Lemma sgn_nonneg : forall n, 0 <= sgn n <-> 0 <= n. Proof. - split. + intros n; split. destruct_sgn n; intros. now apply lt_le_incl. order. @@ -323,7 +323,7 @@ Qed. Lemma sgn_mul : forall n m, sgn (n*m) == sgn n * sgn m. Proof. - intros. destruct_sgn n; nzsimpl. + intros n m. destruct_sgn n; nzsimpl. destruct_sgn m. apply sgn_pos. now apply mul_pos_pos. apply sgn_null. rewrite eq_mul_0; auto with relations. @@ -337,7 +337,7 @@ Qed. Lemma sgn_abs : forall n, n * sgn n == abs n. Proof. - intros. symmetry. + intros n. symmetry. destruct_sgn n; try rewrite mul_opp_r; nzsimpl. apply abs_eq. now apply lt_le_incl. rewrite abs_0_iff; auto with relations. @@ -346,7 +346,7 @@ Qed. Lemma abs_sgn : forall n, abs n * sgn n == n. Proof. - intros. + intros n. destruct_sgn n; try rewrite mul_opp_r; nzsimpl; auto. apply abs_eq. now apply lt_le_incl. rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl. @@ -354,7 +354,7 @@ Qed. Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x. Proof. - intros. + intros x. destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. apply sgn_pos, lt_0_1. now apply sgn_null. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index c155395ecd..06b02ab211 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -128,28 +128,28 @@ Definition nat_of_ascii (a : ascii) : nat := N.to_nat (N_of_ascii a). Theorem ascii_N_embedding : forall a : ascii, ascii_of_N (N_of_ascii a) = a. Proof. - destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. + intro a; destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. Qed. Theorem N_ascii_embedding : forall n:N, (n < 256)%N -> N_of_ascii (ascii_of_N n) = n. Proof. -destruct n. +intro n; destruct n as [|p]. reflexivity. -do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]); +do 8 (destruct p as [p|p|]; [ | | intros; vm_compute; reflexivity ]); intro H; vm_compute in H; destruct p; discriminate. Qed. Theorem N_ascii_bounded : forall a : ascii, (N_of_ascii a < 256)%N. Proof. - destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. + intro a; destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. Qed. Theorem ascii_nat_embedding : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a. Proof. - destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity. + intro a; destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity. Qed. Theorem nat_ascii_embedding : diff --git a/theories/Strings/String.v b/theories/Strings/String.v index a468a4fe87..b792acc9f9 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -54,7 +54,8 @@ Infix "=?" := eqb : string_scope. Lemma eqb_spec s1 s2 : Bool.reflect (s1 = s2) (s1 =? s2)%string. Proof. - revert s2. induction s1; destruct s2; try (constructor; easy); simpl. + revert s2. induction s1 as [|? s1 IHs1]; + intro s2; destruct s2; try (constructor; easy); simpl. case Ascii.eqb_spec; simpl; [intros -> | constructor; now intros [= ]]. case IHs1; [intros ->; now constructor | constructor; now intros [= ]]. Qed. @@ -117,7 +118,7 @@ intros s1; elim s1; simpl. intros s2; case s2; simpl; split; auto. intros H; generalize (H O); intros H1; inversion H1. intros; discriminate. -intros a s1' Rec s2; case s2; simpl; split; auto. +intros a s1' Rec s2; case s2 as [|? s]; simpl; split; auto. intros H; generalize (H O); intros H1; inversion H1. intros; discriminate. intros H; generalize (H O); simpl; intros H1; inversion H1. @@ -249,7 +250,7 @@ intros b s2'; case (ascii_dec a b); simpl; auto. intros e; case (Rec s2'); intros H1 H2; split; intros H3; auto. rewrite e; rewrite H1; auto. apply H2; injection H3; auto. -intros n; split; intros; try discriminate. +intros n; split; intros H; try discriminate. case n; injection H; auto. Qed. diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index 18e286b943..45fcbfb329 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -111,7 +111,7 @@ Qed. Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p. Proof. -induction p; simpl. +induction p as [|? p]; simpl. - reflexivity. - destruct (to_nat p); simpl in *. f_equal. subst p. apply of_nat_ext. Qed. @@ -119,7 +119,7 @@ Qed. Lemma to_nat_of_nat {p}{n} (h : p < n) : to_nat (of_nat_lt h) = exist _ p h. Proof. revert n h. - induction p; (destruct n ; intros h; [ destruct (Lt.lt_n_O _ h) | cbn]); + induction p as [|p IHp]; (intro n; destruct n as [|n]; intros h; [ destruct (Lt.lt_n_O _ h) | cbn]); [ | rewrite (IHp _ (Lt.lt_S_n p n h))]; f_equal; apply Peano_dec.le_unique. Qed. @@ -153,7 +153,7 @@ Fixpoint L {m} n (p : t m) : t (m + n) := Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p). Proof. -induction p. +induction p as [|? p IHp]. - reflexivity. - simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p). Qed. @@ -163,7 +163,7 @@ Qed. Really really inefficient !!! *) Definition L_R {m} n (p : t m) : t (n + m). Proof. -induction n. +induction n as [|n IHn]. - exact p. - exact ((fix LS k (p: t k) := match p with @@ -179,7 +179,7 @@ Fixpoint R {m} n (p : t m) : t (n + m) := Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p). Proof. -induction n. +induction n as [|n IHn]. - reflexivity. - simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p). Qed. @@ -193,7 +193,7 @@ end. Lemma depair_sanity {m n} (o : t m) (p : t n) : proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)). Proof. -induction o ; simpl. +induction o as [|? o IHo] ; simpl. - rewrite L_sanity. now rewrite Mult.mult_0_r. - rewrite R_sanity. rewrite IHo. @@ -211,7 +211,8 @@ end. Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n. Proof. -intros m n p; revert n; induction p; destruct q; simpl; intros; f_equal. +intros m n p; revert n; induction p as [|? p IHp]; + intros ? q; destruct q; simpl; intros; f_equal. - now apply EqNat.beq_nat_true. - easy. - easy. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 57241e5f42..a154a2b269 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -167,7 +167,7 @@ Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n -> t A (n - p). Proof. - induction p as [| p f]; intros H v. + intros A n p; induction p as [| p f]; intros H v. rewrite <- minus_n_O. exact v. diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v index 6bd2c30205..c36917aa90 100644 --- a/theories/Vectors/VectorEq.v +++ b/theories/Vectors/VectorEq.v @@ -36,7 +36,7 @@ Section BEQ. (Hbeq: eqb v1 v2 = true), m = n. Proof. intros m n v1; revert n. - induction v1; destruct v2; + induction v1; intros ? v2; destruct v2; [now constructor | discriminate | discriminate | simpl]. intros Hbeq; apply andb_prop in Hbeq; destruct Hbeq. f_equal; eauto. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 443931e5bb..10545332bb 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -26,7 +26,7 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v. Proof. -intros; apply caseS with (v:=v); intros; reflexivity. +intros; apply (fun P IS => caseS P IS (n := n) v); intros; reflexivity. Defined. (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all @@ -38,9 +38,9 @@ Lemma eq_nth_iff A n (v1 v2: t A n): (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2. Proof. split. -- revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros. +- revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl. + reflexivity. - + f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl). + + intros n ? ? H ? ? H0. f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl). apply H. intros p1 p2 H1; apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)). - intros; now f_equal. @@ -48,12 +48,12 @@ Qed. Lemma nth_order_hd A: forall n (v : t A (S n)) (H : 0 < S n), nth_order v H = hd v. -Proof. intros; now rewrite (eta v). Qed. +Proof. intros n v H; now rewrite (eta v). Qed. Lemma nth_order_tl A: forall n k (v : t A (S n)) (H : k < n) (HS : S k < S n), nth_order (tl v) H = nth_order v HS. Proof. -induction n; intros. +intros n; induction n; intros k v H HS. - inversion H. - rewrite (eta v). unfold nth_order; simpl. @@ -69,7 +69,7 @@ Qed. Lemma nth_order_ext A: forall n k (v : t A n) (H1 H2 : k < n), nth_order v H1 = nth_order v H2. Proof. -intros; unfold nth_order. +intros n k v H1 H2; unfold nth_order. now rewrite (Fin.of_nat_ext H1 H2). Qed. @@ -78,7 +78,7 @@ Qed. Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2): nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2. Proof. -subst k2; induction k1. +subst k2; induction k1 as [n|n k1]. - generalize dependent n. apply caseS ; intros. now simpl. - generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl. Qed. @@ -92,14 +92,14 @@ Lemma shiftrepeat_nth A: forall n k (v: t A (S n)), nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k. Proof. refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ]. -- revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t. +- revert n v; refine (@caseS _ _ _); simpl; intros ? ? t. now destruct t. - revert p H. refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with |S (S n) => fun v => forall p : Fin.t (S n), (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) -> (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p] |_ => fun _ => True end v' with - |[] => I |h :: t => _ end). destruct n0. exact I. now simpl. + |[] => I | cons _ h n t => _ end). destruct n. exact I. now simpl. Qed. Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v. @@ -112,7 +112,7 @@ Qed. Lemma nth_order_replace_eq A: forall n k (v : t A n) a (H1 : k < n) (H2 : k < n), nth_order (replace v (Fin.of_nat_lt H2) a) H1 = a. Proof. -intros n k; revert n; induction k; intros; +intros n k; revert n; induction k as [|k IHk]; intros n v a H1 H2; (destruct n; [ inversion H1 | subst ]). - now rewrite nth_order_hd, (eta v). - rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) H1)), (eta v). @@ -123,7 +123,7 @@ Lemma nth_order_replace_neq A: forall n k1 k2, k1 <> k2 -> forall (v : t A n) a (H1 : k1 < n) (H2 : k2 < n), nth_order (replace v (Fin.of_nat_lt H2) a) H1 = nth_order v H1. Proof. -intros n k1; revert n; induction k1; intros; +intros n k1; revert n; induction k1 as [|k1 IHk1]; intros n k2 H v a H1 H2; (destruct n ; [ inversion H1 | subst ]). - rewrite 2 nth_order_hd. destruct k2; intuition. @@ -137,15 +137,15 @@ Qed. Lemma replace_id A: forall n p (v : t A n), replace v p (nth v p) = v. Proof. -induction p; intros; rewrite 2 (eta v); simpl; auto. +intros n p; induction p as [|? p IHp]; intros v; rewrite 2 (eta v); simpl; auto. now rewrite IHp. Qed. Lemma replace_replace_eq A: forall n p (v : t A n) a b, replace (replace v p a) p b = replace v p b. Proof. -intros. -induction p; rewrite 2 (eta v); simpl; auto. +intros n p v a b. +induction p as [|? p IHp]; rewrite 2 (eta v); simpl; auto. now rewrite IHp. Qed. @@ -161,7 +161,7 @@ apply (Fin.rect2 (fun n p1 p2 => forall v a b, - intros n p1 v; revert n v p1. refine (@rectS _ _ _ _); auto. - intros n p1 p2 IH v; revert n v p1 p2 IH. - refine (@rectS _ _ _ _); simpl; do 6 intro; [ | do 3 intro ]; intro Hneq; + refine (@rectS _ _ _ _); simpl; intro n; [| do 3 intro]; intros ? ? IH p1 p2; intro Hneq; f_equal; apply IH; intros Heq; apply Hneq; now subst. Qed. @@ -177,19 +177,19 @@ Qed. Lemma map_id A: forall n (v : t A n), map (fun x => x) v = v. Proof. -induction v; simpl; [ | rewrite IHv ]; auto. +intros n v; induction v as [|? ? v IHv]; simpl; [ | rewrite IHv ]; auto. Qed. Lemma map_map A B C: forall (f:A->B) (g:B->C) n (v : t A n), map g (map f v) = map (fun x => g (f x)) v. Proof. -induction v; simpl; [ | rewrite IHv ]; auto. +intros f g n v; induction v as [|? ? v IHv]; simpl; [ | rewrite IHv ]; auto. Qed. Lemma map_ext_in A B: forall (f g:A->B) n (v : t A n), (forall a, In a v -> f a = g a) -> map f v = map g v. Proof. -induction v; simpl; auto. +intros f g n v H; induction v as [|? ? v IHv]; simpl; auto. intros; rewrite H by constructor; rewrite IHv; intuition. apply H; now constructor. Qed. @@ -203,7 +203,7 @@ Qed. Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2): (map f v) [@ p1] = f (v [@ p2]). Proof. -subst p2; induction p1. +subst p2; induction p1 as [n|n p1 IHp1]. - revert n v; refine (@caseS _ _ _); now simpl. - revert n v p1 IHp1; refine (@caseS _ _ _); now simpl. Qed. @@ -225,10 +225,10 @@ Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A} {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a. Proof. assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h). -- induction v0. +- intros n0 h v0; induction v0 as [|? ? v0 IHv0]. + now simpl. + intros; simpl. rewrite<- IHv0, assoc. now f_equal. -- induction v. +- induction v as [|? ? v IHv]. + reflexivity. + simpl. intros; now rewrite<- (IHv). Qed. @@ -245,31 +245,31 @@ Qed. (** ** Properties of [take] *) Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. -Proof. +Proof. reflexivity. -Qed. +Qed. Lemma take_idem : forall {A} p n (v:t A n) le le', take p le' (take p le v) = take p le v. -Proof. - induction p; intros n v le le'. - - auto. - - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Proof. + intros A p; induction p as [|p IHp]; intros n v le le'. + - auto. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. Qed. Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v. -Proof. - induction v; intros m w le. - - reflexivity. - - simpl. apply f_equal. apply IHv. +Proof. + intros a n v; induction v as [|? ? v IHv]; intros m w le. + - reflexivity. + - simpl. apply f_equal. apply IHv. Qed. (* Proof is irrelevant for [take] *) Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v. -Proof. - induction p; intros n v le le'. - - reflexivity. - - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Proof. + intros A p; induction p as [|p IHp]; intros n v le le'. + - reflexivity. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. Qed. (** ** Properties of [uncons] and [splitat] *) @@ -289,7 +289,7 @@ Lemma splitat_append {A} : forall {n m : nat} (v : t A n) (w : t A m), Proof with simpl; auto. intros n m v. generalize dependent m. - induction v; intros... + induction v as [|? ? v IHv]; intros... rewrite IHv... Qed. @@ -299,10 +299,10 @@ Lemma append_splitat {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A Proof with auto. intros n m v. generalize dependent m. - induction v; intros; inversion H... + induction v as [|a n v IHv]; intros m w vw H; inversion H as [H1]... destruct (splitat n (tl vw)) as [v' w'] eqn:Heq. apply pair_equal_spec in H1. - destruct H1; subst. + destruct H1 as [H0]; subst. rewrite <- append_comm_cons. rewrite (eta vw). apply cons_inj in H0. @@ -316,7 +316,7 @@ Qed. Lemma Forall_impl A: forall (P Q : A -> Prop), (forall a, P a -> Q a) -> forall n (v : t A n), Forall P v -> Forall Q v. Proof. -induction v; intros HP; constructor; inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; +intros P Q H n v; induction v; intros HP; constructor; inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; intuition. Qed. @@ -328,7 +328,7 @@ intros P n v; split. revert HP; induction Hin; intros HP; inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; subst; auto. apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; auto. -- induction v; intros Hin; constructor. +- induction v as [|? ? v IHv]; intros Hin; constructor. + apply Hin; constructor. + apply IHv; intros a Ha. apply Hin; now constructor. @@ -337,7 +337,7 @@ Qed. Lemma Forall_nth_order A: forall P n (v : t A n), Forall P v <-> forall i (Hi : i < n), P (nth_order v Hi). Proof. -split; induction n. +intros P n v; split; induction n as [|n IHn]. - intros HF i Hi; inversion Hi. - intros HF i Hi. rewrite (eta v). @@ -354,7 +354,7 @@ split; induction n. rewrite (eta v); constructor. + specialize HP with 0 (Nat.lt_0_succ n). now rewrite nth_order_hd in HP. - + apply IHn; intros. + + apply IHn; intros i Hi. specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi). now rewrite <- (nth_order_tl _ _ _ _ Hi) in HP. Qed. @@ -363,7 +363,7 @@ Lemma Forall2_nth_order A: forall P n (v1 v2 : t A n), Forall2 P v1 v2 <-> forall i (Hi1 : i < n) (Hi2 : i < n), P (nth_order v1 Hi1) (nth_order v2 Hi2). Proof. -split; induction n. +intros P n v1 v2; split; induction n as [|n IHn]. - intros HF i Hi1 Hi2; inversion Hi1. - intros HF i Hi1 Hi2. rewrite (eta v1), (eta v2). @@ -382,7 +382,7 @@ split; induction n. rewrite (eta v1), (eta v2); constructor. + specialize HP with 0 (Nat.lt_0_succ _) (Nat.lt_0_succ _). now rewrite nth_order_hd in HP. - + apply IHn; intros. + + apply IHn; intros i Hi1 Hi2. specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi1) (proj1 (Nat.succ_lt_mono _ _) Hi2). now rewrite <- (nth_order_tl _ _ _ _ Hi1), <- (nth_order_tl _ _ _ _ Hi2) in HP. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 9a30e011af..52998c8b95 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -126,7 +126,7 @@ Lemma pos_sub_spec p q : | Gt => pos (p - q) end. Proof. - revert q. induction p; destruct q; simpl; trivial; + revert q. induction p as [p IHp|p IHp|]; intros q; destruct q; simpl; trivial; rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xI_xO, ?Pos.compare_xO_xO, IHp; simpl; case Pos.compare_spec; intros; simpl; trivial; @@ -168,7 +168,7 @@ Qed. Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p. Proof. - revert q; induction p; destruct q; simpl; trivial; + revert q; induction p as [p IHp|p IHp|]; intros q; destruct q; simpl; trivial; rewrite <- IHp; now destruct pos_sub. Qed. @@ -468,13 +468,13 @@ Lemma peano_ind (P : Z -> Prop) : (forall x, P x -> P (pred x)) -> forall z, P z. Proof. - intros H0 Hs Hp z; destruct z. + intros H0 Hs Hp z; destruct z as [|p|p]. assumption. - induction p using Pos.peano_ind. + induction p as [|p IHp] using Pos.peano_ind. now apply (Hs 0). rewrite <- Pos.add_1_r. now apply (Hs (pos p)). - induction p using Pos.peano_ind. + induction p as [|p IHp] using Pos.peano_ind. now apply (Hp 0). rewrite <- Pos.add_1_r. now apply (Hp (neg p)). @@ -486,7 +486,7 @@ Lemma bi_induction (P : Z -> Prop) : (forall x, P x <-> P (succ x)) -> forall z, P z. Proof. - intros _ H0 Hs. induction z using peano_ind. + intros _ H0 Hs z. induction z using peano_ind. assumption. now apply -> Hs. apply Hs. now rewrite succ_pred. @@ -569,7 +569,7 @@ Qed. Lemma sqrtrem_spec n : 0<=n -> let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s. Proof. - destruct n. now repeat split. + destruct n as [|p|p]. now repeat split. generalize (Pos.sqrtrem_spec p). simpl. destruct 1; simpl; subst; now repeat split. now destruct 1. @@ -578,7 +578,7 @@ Qed. Lemma sqrt_spec n : 0<=n -> let s := sqrt n in s*s <= n < (succ s)*(succ s). Proof. - destruct n. now repeat split. unfold sqrt. + destruct n as [|p|p]. now repeat split. unfold sqrt. intros _. simpl succ. rewrite Pos.add_1_r. apply (Pos.sqrt_spec p). now destruct 1. Qed. @@ -590,7 +590,7 @@ Qed. Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n. Proof. - destruct n; try reflexivity. + destruct n as [|p|p]; try reflexivity. unfold sqrtrem, sqrt, Pos.sqrt. destruct (Pos.sqrtrem p) as (s,r). now destruct r. Qed. @@ -655,7 +655,7 @@ Lemma pos_div_eucl_eq a b : 0 < b -> let (q, r) := pos_div_eucl a b in pos a = q * b + r. Proof. intros Hb. - induction a; unfold pos_div_eucl; fold pos_div_eucl. + induction a as [a IHa|a IHa|]; unfold pos_div_eucl; fold pos_div_eucl. - (* ~1 *) destruct pos_div_eucl as (q,r). change (pos a~1) with (2*(pos a)+1). @@ -720,7 +720,7 @@ Proof. now rewrite Pos.add_diag. intros Hb. destruct b as [|b|b]; discriminate Hb || clear Hb. - induction a; unfold pos_div_eucl; fold pos_div_eucl. + induction a as [a IHa|a IHa|]; unfold pos_div_eucl; fold pos_div_eucl. (* ~1 *) destruct pos_div_eucl as (q,r). simpl in IHa; destruct IHa as (Hr,Hr'). @@ -996,7 +996,7 @@ Proof. intros Hn Hm. unfold shiftr. destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl. now rewrite add_0_r. - assert (forall p, to_N (m + pos p) = (to_N m + N.pos p)%N). + assert (forall p, to_N (m + pos p) = (to_N m + N.pos p)%N) as H. destruct m; trivial; now destruct Hm. assert (forall p, 0 <= m + pos p). destruct m; easy || now destruct Hm. @@ -1054,7 +1054,7 @@ Proof. subst. now rewrite N.sub_diag. simpl. destruct (Pos.sub_mask_pos' m n H') as (p & -> & <-). f_equal. now rewrite Pos.add_comm, Pos.add_sub. - destruct a; unfold shiftl. + destruct a as [|p|p]; unfold shiftl. (* ... a = 0 *) replace (Pos.iter (mul 2) 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 62fccf3ce2..9fa05dd2f7 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -67,7 +67,7 @@ Lemma natlike_ind : forall x:Z, 0 <= x -> P x. Proof. intros P Ho Hrec x Hx; apply Z_of_nat_prop; trivial. - induction n. exact Ho. + intros n; induction n. exact Ho. rewrite Nat2Z.inj_succ. apply Hrec; trivial using Nat2Z.is_nonneg. Qed. @@ -78,7 +78,7 @@ Lemma natlike_rec : forall x:Z, 0 <= x -> P x. Proof. intros P Ho Hrec x Hx; apply Z_of_nat_set; trivial. - induction n. exact Ho. + intros n; induction n. exact Ho. rewrite Nat2Z.inj_succ. apply Hrec; trivial using Nat2Z.is_nonneg. Qed. @@ -101,9 +101,9 @@ Section Efficient_Rec. (forall z:Z, 0 <= z -> P z -> P (Z.succ z)) -> forall z:Z, 0 <= z -> P z. Proof. - intros P Ho Hrec. + intros P Ho Hrec z. induction z as [z IH] using (well_founded_induction_type R_wf). - destruct z; intros Hz. + destruct z as [|p|p]; intros Hz. - apply Ho. - set (y:=Z.pred (Zpos p)). assert (LE : 0 <= y) by (unfold y; now apply Z.lt_le_pred). @@ -121,9 +121,9 @@ Section Efficient_Rec. (forall z:Z, 0 < z -> P (Z.pred z) -> P z) -> forall z:Z, 0 <= z -> P z. Proof. - intros P Ho Hrec. + intros P Ho Hrec z. induction z as [z IH] using (well_founded_induction_type R_wf). - destruct z; intros Hz. + destruct z as [|p|p]; intros Hz. - apply Ho. - assert (EQ : 0 <= Z.pred (Zpos p)) by now apply Z.lt_le_pred. apply Hrec. easy. apply IH; trivial. split; trivial. @@ -138,7 +138,7 @@ Section Efficient_Rec. (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) -> forall x:Z, 0 <= x -> P x. Proof. - intros P Hrec. + intros P Hrec x. induction x as [x IH] using (well_founded_induction_type R_wf). destruct x; intros Hx. - apply Hrec; trivial. intros y (Hy,Hy'). @@ -196,7 +196,7 @@ Section Efficient_Rec. (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) -> forall x:Z, z <= x -> P x. Proof. - intros; now apply Zlt_lower_bound_rec with z. + intros P z ? x ?; now apply Zlt_lower_bound_rec with z. Qed. End Efficient_Rec. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 834f16cd9e..dc40f9ea51 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -19,7 +19,7 @@ Local Open Scope Z_scope. (* Trivial, to deprecate? *) Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}. Proof. - induction r; auto. + intros r; induction r; auto. Defined. (* end hide *) @@ -92,7 +92,7 @@ Section decidability. Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}. Proof. intro H. - apply Zcompare_rec with (n := x) (m := y). + apply (Zcompare_rec _ x y). intro. right. elim (Z.compare_eq_iff x y); auto with arith. intro. left. elim (Z.compare_eq_iff x y); auto with arith. intro H1. absurd (x > y); auto with arith. @@ -111,7 +111,7 @@ Proof. assumption. intro. right. - apply Z.le_lt_trans with (m := x). + apply (Z.le_lt_trans _ x). apply Z.ge_le. assumption. assumption. @@ -123,14 +123,14 @@ Proof. case (Zlt_cotrans 0 (x + y) H x). - now left. - right. - apply Z.add_lt_mono_l with (p := x). + apply (Z.add_lt_mono_l _ _ x). now rewrite Z.add_0_r. Defined. Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}. Proof. intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy; - [ right; apply Z.add_lt_mono_l with (p := x); rewrite Z.add_0_r | left ]; + [ right; apply (Z.add_lt_mono_l _ _ x); rewrite Z.add_0_r | left ]; assumption. Defined. @@ -143,7 +143,7 @@ Proof. assumption. intro H0. generalize (Z.ge_le _ _ H0). - intro. + intro H1. case (Z_le_lt_eq_dec _ _ H1). intro. right. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 21086d9b61..f869e15023 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -49,12 +49,12 @@ Qed. Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Z.abs n). Proof. - now destruct n. + intros P n; now destruct n. Qed. Definition Zabs_dec : forall x:Z, {x = Z.abs x} + {x = - Z.abs x}. Proof. - destruct x; auto. + intros x; destruct x; auto. Defined. Lemma Zabs_spec x : diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index c9e1b340a6..c848623d06 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -13,7 +13,6 @@ Require Import ZArith_base. Require Import Wf_nat. Local Open Scope Z_scope. - (**********************************************************************) (** About parity *) @@ -39,7 +38,7 @@ Proof. reflexivity. Qed. Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. Proof. - unfold floor. induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl. + unfold floor. intros p; induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl. - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. split. + apply Z.le_trans with (2 * Z.pos p); auto with zarith. @@ -69,10 +68,10 @@ Proof. apply (Z_lt_rec Q); auto with zarith. subst Q; intros x H. split; apply HP. - - rewrite Z.abs_eq; auto; intros. + - rewrite Z.abs_eq; auto; intros m ?. destruct (H (Z.abs m)); auto with zarith. destruct (Zabs_dec m) as [-> | ->]; trivial. - - rewrite Z.abs_neq, Z.opp_involutive; intros. + - rewrite Z.abs_neq, Z.opp_involutive; [intros m ?|]. + destruct (H (Z.abs m)); auto with zarith. destruct (Zabs_dec m) as [-> | ->]; trivial. + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. @@ -85,15 +84,15 @@ Theorem Z_lt_abs_induction : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. - enough (Q (Z.abs p)) by + enough (Q (Z.abs p)) as H by (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). apply (Z_lt_induction Q); auto with zarith. - subst Q; intros. + subst Q; intros ? H. split; apply HP. - - rewrite Z.abs_eq; auto; intros. + - rewrite Z.abs_eq; auto; intros m ?. 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; intros. + - rewrite Z.abs_neq, Z.opp_involutive; [intros m ?|]. + destruct (H (Z.abs m)); auto with zarith. destruct (Zabs_dec m) as [-> | ->]; trivial. + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. @@ -136,7 +135,7 @@ Section Zlength_properties. Lemma Zlength_correct l : Zlength l = Z.of_nat (length l). Proof. assert (H : forall l acc, Zlength_aux acc A l = acc + Z.of_nat (length l)). - clear l. induction l. + clear l. intros l; induction l as [|? ? IHl]. auto with zarith. intros. simpl length; simpl Zlength_aux. rewrite IHl, Nat2Z.inj_succ, Z.add_succ_comm; auto. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index b6fbe64499..2039dc0bee 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -174,22 +174,22 @@ Proof. intros; eapply Zmod_unique_full; eauto. Qed. Lemma Zmod_0_l: forall a, 0 mod a = 0. Proof. - destruct a; simpl; auto. + intros a; destruct a; simpl; auto. Qed. Lemma Zmod_0_r: forall a, a mod 0 = 0. Proof. - destruct a; simpl; auto. + intros a; destruct a; simpl; auto. Qed. Lemma Zdiv_0_l: forall a, 0/a = 0. Proof. - destruct a; simpl; auto. + intros a; destruct a; simpl; auto. Qed. Lemma Zdiv_0_r: forall a, a/0 = 0. Proof. - destruct a; simpl; auto. + intros a; destruct a; simpl; auto. Qed. Ltac zero_or_not a := @@ -198,10 +198,10 @@ Ltac zero_or_not a := auto with zarith|]. Lemma Zmod_1_r: forall a, a mod 1 = 0. -Proof. intros. zero_or_not a. apply Z.mod_1_r. Qed. +Proof. intros a. zero_or_not a. apply Z.mod_1_r. Qed. Lemma Zdiv_1_r: forall a, a/1 = a. -Proof. intros. zero_or_not a. apply Z.div_1_r. Qed. +Proof. intros a. zero_or_not a. apply Z.div_1_r. Qed. Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r : zarith. @@ -216,10 +216,10 @@ Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1. Proof Z.div_same. Lemma Z_mod_same_full : forall a, a mod a = 0. -Proof. intros. zero_or_not a. apply Z.mod_same; auto. Qed. +Proof. intros a. zero_or_not a. apply Z.mod_same; auto. Qed. Lemma Z_mod_mult : forall a b, (a*b) mod b = 0. -Proof. intros. zero_or_not b. apply Z.mod_mul. auto. Qed. +Proof. intros a b. zero_or_not b. apply Z.mod_mul. auto. Qed. Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a. Proof Z.div_mul. @@ -313,7 +313,7 @@ Proof. intros; apply Z.div_le_compat_l; intuition auto using Z.lt_le_incl. Qed. Theorem Zdiv_sgn: forall a b, 0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b. Proof. - destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; + intros a b; destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl; destruct Z.pos_div_eucl as (q,r); destruct r; rewrite ?Z.mul_1_r, <-?Z.opp_eq_mul_m1, ?Z.sgn_opp, ?Z.opp_involutive; @@ -325,7 +325,7 @@ Qed. (** * Relations between usual operations and Z.modulo and Z.div *) Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c. -Proof. intros. zero_or_not c. apply Z.mod_add; auto. Qed. +Proof. intros a b c. zero_or_not c. apply Z.mod_add; auto. Qed. Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b. Proof Z.div_add. @@ -338,34 +338,34 @@ Proof Z.div_add_l. some of the relations about [Z.opp] and divisions are rather complex. *) Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. -Proof. intros. zero_or_not b. apply Z.div_opp_opp; auto. Qed. +Proof. intros a b. zero_or_not b. apply Z.div_opp_opp; auto. Qed. Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b). -Proof. intros. zero_or_not b. apply Z.mod_opp_opp; auto. Qed. +Proof. intros a b. zero_or_not b. apply Z.mod_opp_opp; auto. Qed. Lemma Z_mod_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a) mod b = 0. -Proof. intros. zero_or_not b. apply Z.mod_opp_l_z; auto. Qed. +Proof. intros a b. zero_or_not b. apply Z.mod_opp_l_z; auto. Qed. Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 -> (-a) mod b = b - (a mod b). -Proof. intros. zero_or_not b. apply Z.mod_opp_l_nz; auto. Qed. +Proof. intros a b. zero_or_not b. apply Z.mod_opp_l_nz; auto. Qed. Lemma Z_mod_zero_opp_r : forall a b:Z, a mod b = 0 -> a mod (-b) = 0. -Proof. intros. zero_or_not b. apply Z.mod_opp_r_z; auto. Qed. +Proof. intros a b. zero_or_not b. apply Z.mod_opp_r_z; auto. Qed. Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 -> a mod (-b) = (a mod b) - b. -Proof. intros. zero_or_not b. apply Z.mod_opp_r_nz; auto. Qed. +Proof. intros a b ?. zero_or_not b. apply Z.mod_opp_r_nz; auto. Qed. Lemma Z_div_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a)/b = -(a/b). -Proof. intros. zero_or_not b. apply Z.div_opp_l_z; auto. Qed. +Proof. intros a b ?. zero_or_not b. apply Z.div_opp_l_z; auto. Qed. Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> (-a)/b = -(a/b)-1. Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_l_nz; auto. Qed. Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b). -Proof. intros. zero_or_not b. apply Z.div_opp_r_z; auto. Qed. +Proof. intros a b ?. zero_or_not b. apply Z.div_opp_r_z; auto. Qed. Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> a/(-b) = -(a/b)-1. @@ -375,19 +375,19 @@ Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_r_nz; auto. Qe Lemma Zdiv_mult_cancel_r : forall a b c:Z, c <> 0 -> (a*c)/(b*c) = a/b. -Proof. intros. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed. +Proof. intros a b c ?. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed. Lemma Zdiv_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)/(c*b) = a/b. Proof. - intros. rewrite (Z.mul_comm c b); zero_or_not b. + intros a b c ?. rewrite (Z.mul_comm c b); zero_or_not b. rewrite (Z.mul_comm b c). apply Z.div_mul_cancel_l; auto. Qed. Lemma Zmult_mod_distr_l: forall a b c, (c*a) mod (c*b) = c * (a mod b). Proof. - intros. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b. + intros a b c. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b. + now rewrite Z.mul_0_r. + rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto. Qed. @@ -395,7 +395,7 @@ Qed. Lemma Zmult_mod_distr_r: forall a b c, (a*c) mod (b*c) = (a mod b) * c. Proof. - intros. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c. + intros a b c. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c. + now rewrite Z.mul_0_r. + rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto. Qed. @@ -403,27 +403,27 @@ Qed. (** Operations modulo. *) Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n. -Proof. intros. zero_or_not n. apply Z.mod_mod; auto. Qed. +Proof. intros a n. zero_or_not n. apply Z.mod_mod; auto. Qed. Theorem Zmult_mod: forall a b n, (a * b) mod n = ((a mod n) * (b mod n)) mod n. -Proof. intros. zero_or_not n. apply Z.mul_mod; auto. Qed. +Proof. intros a b n. zero_or_not n. apply Z.mul_mod; auto. Qed. Theorem Zplus_mod: forall a b n, (a + b) mod n = (a mod n + b mod n) mod n. -Proof. intros. zero_or_not n. apply Z.add_mod; auto. Qed. +Proof. intros a b n. zero_or_not n. apply Z.add_mod; auto. Qed. Theorem Zminus_mod: forall a b n, (a - b) mod n = (a mod n - b mod n) mod n. Proof. - intros. + intros a b n. replace (a - b) with (a + (-1) * b); auto with zarith. replace (a mod n - b mod n) with (a mod n + (-1) * (b mod n)); auto with zarith. rewrite Zplus_mod. rewrite Zmult_mod. - rewrite Zplus_mod with (b:=(-1) * (b mod n)). + rewrite (Zplus_mod _ ((-1) * (b mod n))). rewrite Zmult_mod. - rewrite Zmult_mod with (b:= b mod n). + rewrite (Zmult_mod _ (b mod n)). repeat rewrite Zmod_mod; auto. Qed. @@ -483,17 +483,20 @@ Qed. Instance Zplus_eqm : Proper (eqm ==> eqm ==> eqm) Z.add. Proof. - unfold eqm; repeat red; intros. rewrite Zplus_mod, H, H0, <- Zplus_mod; auto. + unfold eqm; repeat red; intros ? ? H ? ? H0. + rewrite Zplus_mod, H, H0, <- Zplus_mod; auto. Qed. Instance Zminus_eqm : Proper (eqm ==> eqm ==> eqm) Z.sub. Proof. - unfold eqm; repeat red; intros. rewrite Zminus_mod, H, H0, <- Zminus_mod; auto. + unfold eqm; repeat red; intros ? ? H ? ? H0. + rewrite Zminus_mod, H, H0, <- Zminus_mod; auto. Qed. Instance Zmult_eqm : Proper (eqm ==> eqm ==> eqm) Z.mul. Proof. - unfold eqm; repeat red; intros. rewrite Zmult_mod, H, H0, <- Zmult_mod; auto. + unfold eqm; repeat red; intros ? ? H ? ? H0. + rewrite Zmult_mod, H, H0, <- Zmult_mod; auto. Qed. Instance Zopp_eqm : Proper (eqm ==> eqm) Z.opp. @@ -503,7 +506,7 @@ Qed. Lemma Zmod_eqm : forall a, (a mod N) == a. Proof. - intros; exact (Zmod_mod a N). + intros a; exact (Zmod_mod a N). Qed. (* NB: Z.modulo and Z.div are not morphisms with respect to eqm. @@ -518,7 +521,7 @@ End EqualityModulo. Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c). Proof. - intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. + intros a b c ? ?. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. rewrite Z.mul_comm. apply Z.div_div; auto. apply Z.le_neq; auto. Qed. @@ -538,7 +541,7 @@ Qed. Theorem Zdiv_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. - intros. zero_or_not b. now rewrite Z.mul_0_r. + intros a b c ? ? ?. zero_or_not b. now rewrite Z.mul_0_r. apply Z.div_mul_le; auto. apply Z.le_neq; auto. Qed. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 6a82645ba6..7f72d42d1f 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -50,7 +50,7 @@ Qed. Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n. Proof. - destruct n; trivial. simpl. + destruct n as [|p]; trivial. simpl. destruct (Pos2Nat.is_succ p) as (m,H). rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv. Qed. @@ -668,7 +668,7 @@ Qed. Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z. Proof. - destruct z; simpl; trivial; + destruct z as [|p|p]; simpl; trivial; destruct (Pos2Nat.is_succ p) as (n,H); rewrite H; simpl; f_equal; now apply SuccNat2Pos.inv. Qed. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 6ba58df721..cad9454906 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -256,15 +256,15 @@ Qed. Lemma Zis_gcd_for_euclid : forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d. Proof. - simple induction 1; constructor; intuition. + intros a b d q; simple induction 1; constructor; intuition. replace a with (a - q * b + q * b). auto with zarith. ring. Qed. Lemma Zis_gcd_for_euclid2 : forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d. Proof. - simple induction 1; constructor; intuition. - apply H2; auto. + intros b d q r; destruct 1 as [? ? H]; constructor; intuition. + apply H; auto. replace r with (b * q + r - b * q). auto with zarith. ring. Qed. @@ -300,9 +300,9 @@ Section extended_euclid_algorithm. Proof. intros v3 Hv3; generalize Hv3; pattern v3. apply Zlt_0_rec. - clear v3 Hv3; intros. + clear v3 Hv3; intros x H ? ? u1 u2 u3 v1 v2 H1 H2 H3. destruct (Z_zerop x) as [Heq|Hneq]. - apply Euclid_intro with (u := u1) (v := u2) (d := u3). + apply (Euclid_intro u1 u2 u3). assumption. apply H3. rewrite Heq; auto with zarith. @@ -333,12 +333,10 @@ Section extended_euclid_algorithm. Proof. case (Z_le_gt_dec 0 b); intro. intros; - apply euclid_rec with - (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b); + apply (fun H => euclid_rec b H 1 0 a 0 1); auto; ring. intros; - apply euclid_rec with - (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b); + apply (fun H => euclid_rec (- b) H 1 0 a 0 (-1)); auto; try ring. now apply Z.opp_nonneg_nonpos, Z.lt_le_incl, Z.gt_lt. auto with zarith. @@ -349,8 +347,8 @@ End extended_euclid_algorithm. Theorem Zis_gcd_uniqueness_apart_sign : forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'. Proof. - simple induction 1. - intros H1 H2 H3; simple induction 1; intros. + intros a b d d'; simple induction 1. + intros H1 H2 H3; destruct 1 as [H4 H5 H6]. generalize (H3 d' H4 H5); intro Hd'd. generalize (H6 d H1 H2); intro Hdd'. exact (Z.divide_antisym d d' Hdd' Hd'd). @@ -368,7 +366,7 @@ Proof. intros a b d Hgcd. elim (euclid a b); intros u v d0 e g. generalize (Zis_gcd_uniqueness_apart_sign a b d d0 Hgcd g). - intro H; elim H; clear H; intros. + intro H; elim H; clear H; intros H. apply Bezout_intro with u v. rewrite H; assumption. apply Bezout_intro with (- u) (- v). @@ -380,7 +378,7 @@ Qed. Lemma Zis_gcd_mult : forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d). Proof. - intros a b c d; simple induction 1. constructor; auto with zarith. + intros a b c d; intro H; generalize H; simple induction 1. constructor; auto with zarith. intros x Ha Hb. elim (Zis_gcd_bezout a b d H). intros u v Huv. elim Ha; intros a' Ha'. @@ -407,7 +405,7 @@ Qed. Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b. Proof. - simple induction 1; constructor; auto with zarith. + simple induction 1; intros ? ? H0; constructor; auto with zarith. intros. rewrite <- H0; auto with zarith. Qed. @@ -416,7 +414,7 @@ Qed. Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c). Proof. - intros. elim (rel_prime_bezout a b H0); intros. + intros a b c H H0. elim (rel_prime_bezout a b H0); intros u v H1. replace c with (c * 1); [ idtac | ring ]. rewrite <- H1. replace (c * (u * a + v * b)) with (c * u * a + v * (b * c)); @@ -429,11 +427,11 @@ Lemma rel_prime_mult : forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c). Proof. intros a b c Hb Hc. - elim (rel_prime_bezout a b Hb); intros. - elim (rel_prime_bezout a c Hc); intros. + elim (rel_prime_bezout a b Hb); intros u v H. + elim (rel_prime_bezout a c Hc); intros u0 v0 H0. apply bezout_rel_prime. - apply Bezout_intro with - (u := u * u0 * a + v0 * c * u + u0 * v * b) (v := v * v0). + apply (Bezout_intro _ _ _ + (u * u0 * a + v0 * c * u + u0 * v * b) (v * v0)). rewrite <- H. replace (u * a + v * b) with ((u * a + v * b) * 1); [ idtac | ring ]. rewrite <- H0. @@ -447,7 +445,7 @@ Lemma rel_prime_cross_prod : Proof. intros a b c d; intros H H0 H1 H2 H3. elim (Z.divide_antisym b d). - - split; auto with zarith. + - intros H4; split; auto with zarith. rewrite H4 in H3. rewrite Z.mul_comm in H3. apply Z.mul_reg_l with d; auto. @@ -473,9 +471,9 @@ Lemma Zis_gcd_rel_prime : Proof. intros a b g; intros H H0 H1. assert (H2 : g <> 0) by - (intro; - elim H1; intros; - elim H4; intros; + (intro H2; + elim H1; intros ? H4 ?; + elim H4; intros ? H6; rewrite H2 in H6; subst b; contradict H; rewrite Z.mul_0_r; discriminate). assert (H3 : g > 0) by @@ -578,7 +576,7 @@ Lemma prime_divisors : forall p:Z, prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p. Proof. - destruct 1; intros. + intros p; destruct 1 as [H H0]; intros a ?. assert (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). { assert (Z.abs a <= Z.abs p) as H2. @@ -602,12 +600,13 @@ Proof. } intuition idtac. (* -p < a < -1 *) - - absurd (rel_prime (- a) p). + - match goal with [hyp : a < -1 |- _] => rename hyp into H4 end. + absurd (rel_prime (- a) p). + intros [H1p H2p H3p]. assert (- a | - a) by auto with zarith. - assert (- a | p) by auto with zarith. + assert (- a | p) as H5 by auto with zarith. apply H3p, Z.divide_1_r in H5; auto with zarith. - destruct H5. + destruct H5 as [H5|H5]. * contradict H4; rewrite <- (Z.opp_involutive a), H5 . apply Z.lt_irrefl. * contradict H4; rewrite <- (Z.opp_involutive a), H5 . @@ -616,16 +615,18 @@ Proof. * now apply Z.opp_le_mono; rewrite Z.opp_involutive; apply Z.lt_le_incl. * now apply Z.opp_lt_mono; rewrite Z.opp_involutive. (* a = 0 *) - - contradict H. + - match goal with [hyp : a = 0 |- _] => rename hyp into H2 end. + contradict H. replace p with 0; try discriminate. now apply sym_equal, Z.divide_0_l; rewrite <-H2. (* 1 < a < p *) - - absurd (rel_prime a p). + - match goal with [hyp : 1 < a |- _] => rename hyp into H3 end. + absurd (rel_prime a p). + intros [H1p H2p H3p]. assert (a | a) by auto with zarith. - assert (a | p) by auto with zarith. + assert (a | p) as H5 by auto with zarith. apply H3p, Z.divide_1_r in H5; auto with zarith. - destruct H5. + destruct H5 as [H5|H5]. * contradict H3; rewrite <- (Z.opp_involutive a), H5 . apply Z.lt_irrefl. * contradict H3; rewrite <- (Z.opp_involutive a), H5 . @@ -639,7 +640,7 @@ Qed. Lemma prime_rel_prime : forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a. Proof. - intros; constructor; intros; auto with zarith. + intros p H a H0; constructor; auto with zarith; intros ? H1 H2. apply prime_divisors in H1; intuition; subst; auto with zarith. - absurd (p | a); auto with zarith. - absurd (p | a); intuition. @@ -671,7 +672,7 @@ Qed. Lemma prime_mult : forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b). Proof. - intro p; simple induction 1; intros. + intro p; simple induction 1; intros ? ? a b ?. case (Zdivide_dec p a); intuition. right; apply Gauss with a; auto with zarith. Qed. @@ -743,9 +744,9 @@ Proof. + now exists 1. + elim (H x); auto. split; trivial. - apply Z.le_lt_trans with n; try intuition. + apply Z.le_lt_trans with n; try tauto. apply Z.divide_pos_le; auto with zarith. - apply Z.lt_le_trans with (2 := H0); red; auto. + apply Z.lt_le_trans with (2 := proj1 Hn); red; auto. - (* prime' -> prime *) constructor; trivial. intros n Hn Hnp. case (Zis_gcd_unique n p n 1). @@ -870,7 +871,7 @@ Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith. Theorem Zgcd_1_rel_prime : forall a b, Z.gcd a b = 1 <-> rel_prime a b. Proof. - unfold rel_prime; split; intro H. + unfold rel_prime; intros a b; split; intro H. rewrite <- H; apply Zgcd_is_gcd. case (Zis_gcd_unique a b (Z.gcd a b) 1); auto. apply Zgcd_is_gcd. @@ -894,10 +895,10 @@ Definition prime_dec_aux: Proof. intros p m. case (Z_lt_dec 1 m); intros H1; - [ | left; intros; exfalso; + [ | left; intros n ?; exfalso; contradict H1; apply Z.lt_trans with n; intuition]. pattern m; apply natlike_rec; auto with zarith. - - left; intros; exfalso. + - left; intros n ?; exfalso. absurd (1 < 0); try discriminate. apply Z.lt_trans with n; intuition. - intros x Hx IH; destruct IH as [F|E]. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 7e33fe2b4c..949a01860f 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -354,7 +354,7 @@ Qed. Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n. Proof. - induction n; simpl; intros. apply Z.le_refl. easy. + intros n; induction n; simpl; intros. apply Z.le_refl. easy. Qed. Hint Immediate Z.eq_le_incl: zarith. diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 8609a6af98..d4f58c3b04 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -25,9 +25,9 @@ Notation Zpower_Ppow := Pos2Z.inj_pow (only parsing). Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow. Proof. - constructor. intros. - destruct n;simpl;trivial. + constructor. intros z n. + destruct n as [|p];simpl;trivial. unfold Z.pow_pos. rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1. - induction p; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. + induction p as [p IHp|p IHp|]; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. Qed. diff --git a/theories/micromega/EnvRing.v b/theories/micromega/EnvRing.v index 7bef11e89a..bb21472e57 100644 --- a/theories/micromega/EnvRing.v +++ b/theories/micromega/EnvRing.v @@ -557,7 +557,8 @@ Section MakeRingPol. Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l. Proof. - revert P';induction P;destruct P';simpl; intros H l; try easy. + revert P';induction P as [|p P IHP|P2 IHP1 p P3 IHP2]; + intro P';destruct P' as [|p0 P'|P'1 p0 P'2];simpl; intros H l; try easy. - now apply (morph_eq CRmorph). - destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. now rewrite IHP. @@ -587,7 +588,7 @@ Section MakeRingPol. Lemma env_morph p e1 e2 : (forall x, e1 x = e2 x) -> p @ e1 = p @ e2. Proof. - revert e1 e2. induction p ; simpl. + revert e1 e2. induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - intros e1 e2 EQ. apply IHp. intros. apply EQ. - intros e1 e2 EQ. f_equal; [f_equal|]. @@ -664,13 +665,13 @@ Qed. Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c]. Proof. - revert l;induction P;simpl;intros;Esimpl;trivial. + revert l;induction P as [| |? ? ? ? IHP2];simpl;intros;Esimpl;trivial. rewrite IHP2;rsimpl. Qed. Lemma PsubC_ok c P l : (PsubC P c)@l == P@l - [c]. Proof. - revert l;induction P;simpl;intros. + revert l;induction P as [|? ? IHP|? ? ? ? IHP2];simpl;intros. - Esimpl. - rewrite IHP;rsimpl. - rewrite IHP2;rsimpl. @@ -678,7 +679,7 @@ Qed. Lemma PmulC_aux_ok c P l : (PmulC_aux P c)@l == P@l * [c]. Proof. - revert l;induction P;simpl;intros;Esimpl;trivial. + revert l;induction P as [| |? IHP1 ? ? IHP2];simpl;intros;Esimpl;trivial. rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut. Qed. @@ -694,7 +695,7 @@ Qed. Lemma Popp_ok P l : (--P)@l == - P@l. Proof. - revert l;induction P;simpl;intros. + revert l;induction P as [|? ? IHP|? IHP1 ? ? IHP2];simpl;intros. - Esimpl. - apply IHP. - rewrite IHP1, IHP2;rsimpl. @@ -707,7 +708,7 @@ Qed. (PaddX Padd P' k P) @ l == P@l + P'@l * (hd l)^k. Proof. intros IHP'. - revert k l. induction P;simpl;intros. + revert k l. induction P as [|p|? IHP1];simpl;intros. - add_permut. - destruct p; simpl; rewrite ?Pjump_xO_tail, ?Pjump_pred_double; add_permut. @@ -719,8 +720,8 @@ Qed. Lemma Padd_ok P' P l : (P ++ P')@l == P@l + P'@l. Proof. - revert P l; induction P';simpl;intros;Esimpl. - - revert p l; induction P;simpl;intros. + revert P l; induction P' as [|p P' IHP'|? IHP'1 ? ? IHP'2];simpl;intros P l;Esimpl. + - revert p l; induction P as [|? P IHP|? IHP1 p ? IHP2];simpl;intros p0 l. + Esimpl; add_permut. + destr_pos_sub; intros ->;Esimpl. * now rewrite IHP'. @@ -730,7 +731,7 @@ Qed. * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl. * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl. * rewrite IHP'. rsimpl. - - destruct P;simpl. + - destruct P as [|p0|];simpl. + Esimpl. add_permut. + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. * rewrite Pjump_xO_tail. rsimpl. add_permut. @@ -749,7 +750,7 @@ Qed. (PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k. Proof. intros IHP'. - revert k l. induction P;simpl;intros. + revert k l. induction P as [|p|? IHP1];simpl;intros. - rewrite Popp_ok;rsimpl; add_permut. - destruct p; simpl; rewrite Popp_ok;rsimpl; @@ -762,8 +763,8 @@ Qed. Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l. Proof. - revert P l; induction P';simpl;intros;Esimpl. - - revert p l; induction P;simpl;intros. + revert P l; induction P' as [|p P' IHP'|? IHP'1 ? ? IHP'2];simpl;intros P l;Esimpl. + - revert p l; induction P as [|? ? IHP|? IHP1 ? ? IHP2];simpl;intros p0 l. + Esimpl; add_permut. + destr_pos_sub; intros ->;Esimpl. * rewrite IHP';rsimpl. @@ -773,7 +774,7 @@ Qed. * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl. * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl. * rewrite IHP'. rsimpl. - - destruct P;simpl. + - destruct P as [|p0|];simpl. + Esimpl; add_permut. + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. * rewrite Pjump_xO_tail. rsimpl. add_permut. @@ -791,8 +792,8 @@ Qed. (forall P l, (Pmul P P') @ l == P @ l * P' @ l) -> forall P p l, (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). Proof. - intros IHP'. - induction P;simpl;intros. + intros IHP' P. + induction P as [|? ? IHP|? IHP1 ? ? IHP2];simpl;intros p0 l. - Esimpl; mul_permut. - destr_pos_sub; intros ->;Esimpl. + now rewrite IHP'. @@ -806,10 +807,10 @@ Qed. Lemma Pmul_ok P P' l : (P**P')@l == P@l * P'@l. Proof. - revert P l;induction P';simpl;intros. + revert P l;induction P' as [| |? IHP'1 ? ? IHP'2];simpl;intros P l. - apply PmulC_ok. - apply PmulI_ok;trivial. - - destruct P. + - destruct P as [|p0|]. + rewrite (ARmul_comm ARth). Esimpl. + Esimpl. rewrite IHP'1;Esimpl. f_equiv. destruct p0;rewrite IHP'2;Esimpl. @@ -823,7 +824,7 @@ Qed. Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l. Proof. - revert l;induction P;simpl;intros;Esimpl. + revert l;induction P as [|? ? IHP|P2 IHP1 p ? IHP2];simpl;intros l;Esimpl. - apply IHP. - rewrite Padd_ok, Pmul_ok;Esimpl. rewrite IHP1, IHP2. @@ -833,7 +834,7 @@ Qed. Lemma Mphi_morph M e1 e2 : (forall x, e1 x = e2 x) -> M @@ e1 = M @@ e2. Proof. - revert e1 e2; induction M; simpl; intros e1 e2 EQ; trivial. + revert e1 e2; induction M as [|? ? IHM|? ? IHM]; simpl; intros e1 e2 EQ; trivial. - apply IHM. intros; apply EQ. - f_equal. * apply IHM. intros; apply EQ. @@ -890,7 +891,8 @@ Qed. let (Q,R) := MFactor P M in P@l == Q@l + M@@l * R@l. Proof. - revert M l; induction P; destruct M; intros l; simpl; auto; Esimpl. + revert M l; induction P as [|? ? IHP|? IHP1 ? ? IHP2]; + intros M; destruct M; intros l; simpl; auto; Esimpl. - case Pos.compare_spec; intros He; simpl. * destr_mfactor R1 S1. now rewrite IHP, He, !mkPinj_ok. * destr_mfactor R1 S1. rewrite IHP; simpl. @@ -922,7 +924,7 @@ Qed. Lemma PNSubst1_ok n P1 M1 P2 l : M1@@l == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l. Proof. - revert P1. induction n; simpl; intros P1; + revert P1. induction n as [|n IHn]; simpl; intros P1; generalize (POneSubst_ok P1 M1 P2); destruct POneSubst; intros; rewrite <- ?IHn; auto; reflexivity. Qed. @@ -953,7 +955,7 @@ Qed. Lemma PSubstL_ok n LM1 P1 P2 l : PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l. Proof. - revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. + revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros P3 H **. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. @@ -963,7 +965,7 @@ Qed. Lemma PNSubstL_ok m n LM1 P1 l : MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l. Proof. - revert LM1 P1. induction m; simpl; intros; + revert LM1 P1. induction m as [|m IHm]; simpl; intros LM1 P2 **; assert (H' := PSubstL_ok n LM1 P2); destruct PSubstL; auto; try reflexivity. rewrite <- IHm; auto. @@ -1017,7 +1019,7 @@ Section POWER. forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l. Proof. intros subst_l_ok res P p. revert res. - induction p;simpl;intros; rewrite ?subst_l_ok, ?Pmul_ok, ?IHp; + induction p as [p IHp|p IHp|];simpl;intros; rewrite ?subst_l_ok, ?Pmul_ok, ?IHp; mul_permut. Qed. @@ -1025,7 +1027,7 @@ Section POWER. (forall P, subst_l P@l == P@l) -> forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. Proof. - destruct n;simpl. + intros ? P n;destruct n;simpl. - reflexivity. - rewrite Ppow_pos_ok by trivial. Esimpl. Qed. @@ -1092,7 +1094,7 @@ Section POWER. PEeval l pe == (norm_aux pe)@l. Proof. intros. - induction pe. + induction pe as [| |pe1 IHpe1 pe2 IHpe2|? IHpe1 ? IHpe2|? IHpe1 ? IHpe2|? IHpe|? IHpe n0]. - reflexivity. - apply mkX_ok. - simpl PEeval. rewrite IHpe1, IHpe2. @@ -1104,8 +1106,8 @@ Section POWER. - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok. - simpl. rewrite IHpe. Esimpl. - simpl. rewrite Ppow_N_ok by reflexivity. - rewrite (rpow_pow_N pow_th). destruct n0; simpl; Esimpl. - induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. + rewrite (rpow_pow_N pow_th). destruct n0 as [|p]; simpl; Esimpl. + induction p as [p IHp|p IHp|];simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. Qed. End NORM_SUBST_REC. diff --git a/theories/micromega/OrderedRing.v b/theories/micromega/OrderedRing.v index ea9b20847b..5fa3740ab1 100644 --- a/theories/micromega/OrderedRing.v +++ b/theories/micromega/OrderedRing.v @@ -235,13 +235,13 @@ Qed. Theorem Rle_lt_trans : forall n m p : R, n <= m -> m < p -> n < p. Proof. intros n m p H1 H2; le_elim H1. -now apply Rlt_trans with (m := m). now rewrite H1. +now apply (Rlt_trans (m := m)). now rewrite H1. Qed. Theorem Rlt_le_trans : forall n m p : R, n < m -> m <= p -> n < p. Proof. intros n m p H1 H2; le_elim H2. -now apply Rlt_trans with (m := m). now rewrite <- H2. +now apply (Rlt_trans (m := m)). now rewrite <- H2. Qed. Theorem Rle_gt_cases : forall n m : R, n <= m \/ m < n. diff --git a/theories/micromega/Refl.v b/theories/micromega/Refl.v index 1189309af1..0f82f9e578 100644 --- a/theories/micromega/Refl.v +++ b/theories/micromega/Refl.v @@ -31,7 +31,7 @@ Fixpoint make_impl (A : Type) (eval : A -> Prop) (l : list A) (goal : Prop) {str Theorem make_impl_true : forall (A : Type) (eval : A -> Prop) (l : list A), make_impl eval l True. Proof. -induction l as [| a l IH]; simpl. +intros A eval l; induction l as [| a l IH]; simpl. trivial. intro; apply IH. Qed. @@ -42,9 +42,9 @@ Theorem make_impl_map : (EVAL : forall x, eval' x <-> eval (fst x)), make_impl eval' l r <-> make_impl eval (List.map fst l) r. Proof. -induction l as [| a l IH]; simpl. +intros A B eval eval' l; induction l as [| a l IH]; simpl. - tauto. -- intros. +- intros r EVAL. rewrite EVAL. rewrite IH. tauto. @@ -61,18 +61,18 @@ Fixpoint make_conj (A : Type) (eval : A -> Prop) (l : list A) {struct l} : Prop Theorem make_conj_cons : forall (A : Type) (eval : A -> Prop) (a : A) (l : list A), make_conj eval (a :: l) <-> eval a /\ make_conj eval l. Proof. -intros; destruct l; simpl; tauto. +intros A eval a l; destruct l; simpl; tauto. Qed. Lemma make_conj_impl : forall (A : Type) (eval : A -> Prop) (l : list A) (g : Prop), (make_conj eval l -> g) <-> make_impl eval l g. Proof. - induction l. + intros A eval l; induction l as [|? l IHl]. simpl. tauto. simpl. - intros. + intros g. destruct l. simpl. tauto. @@ -83,11 +83,11 @@ Qed. Lemma make_conj_in : forall (A : Type) (eval : A -> Prop) (l : list A), make_conj eval l -> (forall p, In p l -> eval p). Proof. - induction l. + intros A eval l; induction l as [|? l IHl]. simpl. tauto. simpl. - intros. + intros H ? H0. destruct l. simpl in H0. destruct H0. @@ -101,10 +101,10 @@ Qed. Lemma make_conj_app : forall A eval l1 l2, @make_conj A eval (l1 ++ l2) <-> @make_conj A eval l1 /\ @make_conj A eval l2. Proof. - induction l1. + intros A eval l1; induction l1 as [|a l1 IHl1]. simpl. tauto. - intros. + intros l2. change ((a::l1) ++ l2) with (a :: (l1 ++ l2)). rewrite make_conj_cons. rewrite IHl1. @@ -116,7 +116,7 @@ Infix "+++" := rev_append (right associativity, at level 60) : list_scope. Lemma make_conj_rapp : forall A eval l1 l2, @make_conj A eval (l1 +++ l2) <-> @make_conj A eval (l1++l2). Proof. - induction l1. + intros A eval l1; induction l1 as [|? ? IHl1]. - simpl. tauto. - intros. simpl rev_append at 1. @@ -141,10 +141,10 @@ Lemma not_make_conj_app : forall (A:Type) (t:list A) a eval (no_middle_eval : forall d, eval d \/ ~ eval d) , ~ make_conj eval (t ++ a) <-> (~ make_conj eval t) \/ (~ make_conj eval a). Proof. - induction t. + intros A t; induction t as [|a t IHt]. - simpl. tauto. - - intros. + - intros a0 **. simpl ((a::t)++a0). rewrite !not_make_conj_cons by auto. rewrite IHt by auto. diff --git a/theories/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v index f7a848d7a5..b5289b5800 100644 --- a/theories/micromega/RingMicromega.v +++ b/theories/micromega/RingMicromega.v @@ -215,7 +215,7 @@ Lemma OpMult_sound : forall (o o' om: Op1) (x y : R), eval_op1 o x -> eval_op1 o' y -> OpMult o o' = Some om -> eval_op1 om (x * y). Proof. -unfold eval_op1; destruct o; simpl; intros o' om x y H1 H2 H3. +unfold eval_op1; intros o; destruct o; simpl; intros o' om x y H1 H2 H3. (* x == 0 *) inversion H3. rewrite H1. now rewrite (Rtimes_0_l sor). (* x ~= 0 *) @@ -246,9 +246,9 @@ Lemma OpAdd_sound : forall (o o' oa : Op1) (e e' : R), eval_op1 o e -> eval_op1 o' e' -> OpAdd o o' = Some oa -> eval_op1 oa (e + e'). Proof. -unfold eval_op1; destruct o; simpl; intros o' oa e e' H1 H2 Hoa. +unfold eval_op1; intros o; destruct o; simpl; intros o' oa e e' H1 H2 Hoa. (* e == 0 *) -inversion Hoa. rewrite <- H0. +inversion Hoa as [H0]. rewrite <- H0. destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor). (* e ~= 0 *) destruct o'. @@ -373,8 +373,8 @@ Lemma pexpr_times_nformula_correct : forall (env: PolEnv) (e: PolC) (f f' : NFor eval_nformula env f'. Proof. unfold pexpr_times_nformula. - destruct f. - intros. destruct o ; inversion H0 ; try discriminate. + intros env e f; destruct f as [? o]. + intros f' H H0. destruct o ; inversion H0 ; try discriminate. simpl in *. unfold eval_pol in *. rewrite (Pmul_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)). @@ -388,9 +388,9 @@ Lemma nformula_times_nformula_correct : forall (env:PolEnv) eval_nformula env f. Proof. unfold nformula_times_nformula. - destruct f1 ; destruct f2. + intros env f1 f2; destruct f1 as [? o]; destruct f2 as [? o0]. case_eq (OpMult o o0) ; simpl ; try discriminate. - intros. inversion H2 ; simpl. + intros o1 H ? H0 H1 H2. inversion H2 ; simpl. unfold eval_pol. destruct o1; simpl; rewrite (Pmul_ok (SORsetoid sor) Rops_wd @@ -405,9 +405,9 @@ Lemma nformula_plus_nformula_correct : forall (env:PolEnv) eval_nformula env f. Proof. unfold nformula_plus_nformula. - destruct f1 ; destruct f2. + intros env f1 f2; destruct f1 as [? o] ; destruct f2 as [? o0]. case_eq (OpAdd o o0) ; simpl ; try discriminate. - intros. inversion H2 ; simpl. + intros o1 H ? H0 H1 H2. inversion H2 ; simpl. unfold eval_pol. destruct o1; simpl; rewrite (Padd_ok (SORsetoid sor) Rops_wd @@ -421,9 +421,10 @@ Lemma eval_Psatz_Sound : forall (e : Psatz) (f : NFormula), eval_Psatz l e = Some f -> eval_nformula env f. Proof. - induction e. + intros l env H e; + induction e as [n|?|? e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2|c|]. (* PsatzIn *) - simpl ; intros. + simpl ; intros f H0. destruct (nth_in_or_default n l (Pc cO, Equal)) as [Hin|Heq]. (* index is in bounds *) apply H. congruence. @@ -432,7 +433,7 @@ Proof. rewrite Heq. simpl. now apply (morph0 (SORrm addon)). (* PsatzSquare *) - simpl. intros. inversion H0. + simpl. intros ? H0. inversion H0. simpl. unfold eval_pol. rewrite (Psquare_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)); @@ -440,7 +441,7 @@ Proof. (* PsatzMulC *) simpl. intro. - case_eq (eval_Psatz l e) ; simpl ; intros. + case_eq (eval_Psatz l e) ; simpl ; intros ? H0; [intros H1|]. apply IHe in H0. apply pexpr_times_nformula_correct with (1:=H0) (2:= H1). discriminate. @@ -448,24 +449,24 @@ Proof. simpl ; intro. case_eq (eval_Psatz l e1) ; simpl ; try discriminate. case_eq (eval_Psatz l e2) ; simpl ; try discriminate. - intros. + intros n H0 n0 H1 ?. apply IHe1 in H1. apply IHe2 in H0. apply (nformula_times_nformula_correct env n0 n) ; assumption. (* PsatzAdd *) simpl ; intro. case_eq (eval_Psatz l e1) ; simpl ; try discriminate. case_eq (eval_Psatz l e2) ; simpl ; try discriminate. - intros. + intros n H0 n0 H1 ?. apply IHe1 in H1. apply IHe2 in H0. apply (nformula_plus_nformula_correct env n0 n) ; assumption. (* PsatzC *) simpl. intro. case_eq (cO [<] c). - intros. inversion H1. simpl. + intros H0 H1. inversion H1. simpl. rewrite <- (morph0 (SORrm addon)). now apply cltb_sound. discriminate. (* PsatzZ *) - simpl. intros. inversion H0. + simpl. intros ? H0. inversion H0. simpl. apply (morph0 (SORrm addon)). Qed. @@ -484,7 +485,8 @@ Fixpoint ge_bool (n m : nat) : bool := Lemma ge_bool_cases : forall n m, (if ge_bool n m then n >= m else n < m)%nat. Proof. - induction n; destruct m ; simpl; auto with arith. + intros n; induction n as [|n IHn]; + intros m; destruct m as [|m]; simpl; auto with arith. specialize (IHn m). destruct (ge_bool); auto with arith. Qed. @@ -511,26 +513,27 @@ Fixpoint extract_hyps (l: list NFormula) (ln : list nat) : list NFormula := | nil => nil | n::ln => nth n l (Pc cO, Equal) :: extract_hyps l ln end. - + Lemma extract_hyps_app : forall l ln1 ln2, extract_hyps l (ln1 ++ ln2) = (extract_hyps l ln1) ++ (extract_hyps l ln2). Proof. - induction ln1. + intros l ln1; induction ln1 as [|? ln1 IHln1]. reflexivity. simpl. intros. rewrite IHln1. reflexivity. Qed. - + Ltac inv H := inversion H ; try subst ; clear H. Lemma nhyps_of_psatz_correct : forall (env : PolEnv) (e:Psatz) (l : list NFormula) (f: NFormula), - eval_Psatz l e = Some f -> + eval_Psatz l e = Some f -> ((forall f', In f' (extract_hyps l (nhyps_of_psatz e)) -> eval_nformula env f') -> eval_nformula env f). Proof. - induction e ; intros. + intros env e; induction e as [n|?|? e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2|c|]; + intros l f H H0. (*PsatzIn*) - simpl in *. + simpl in *. apply H0. intuition congruence. (* PsatzSquare *) simpl in *. @@ -543,15 +546,15 @@ Proof. (* PsatzMulC *) simpl in *. case_eq (eval_Psatz l e). - intros. rewrite H1 in H. simpl in H. + intros ? H1. rewrite H1 in H. simpl in H. apply pexpr_times_nformula_correct with (2:= H). apply IHe with (1:= H1); auto. - intros. rewrite H1 in H. simpl in H ; discriminate. + intros H1. rewrite H1 in H. simpl in H ; discriminate. (* PsatzMulE *) simpl in *. revert H. case_eq (eval_Psatz l e1). - case_eq (eval_Psatz l e2) ; simpl ; intros. + case_eq (eval_Psatz l e2) ; simpl ; intros ? H ? H1; [intros H2|]. apply nformula_times_nformula_correct with (3:= H2). apply IHe1 with (1:= H1) ; auto. intros. apply H0. rewrite extract_hyps_app. @@ -564,7 +567,7 @@ Proof. simpl in *. revert H. case_eq (eval_Psatz l e1). - case_eq (eval_Psatz l e2) ; simpl ; intros. + case_eq (eval_Psatz l e2) ; simpl ; intros ? H ? H1; [intros H2|]. apply nformula_plus_nformula_correct with (3:= H2). apply IHe1 with (1:= H1) ; auto. intros. apply H0. rewrite extract_hyps_app. @@ -576,16 +579,16 @@ Proof. (* PsatzC *) simpl in H. case_eq (cO [<] c). - intros. rewrite H1 in H. inv H. + intros H1. rewrite H1 in H. inv H. unfold eval_nformula. simpl. rewrite <- (morph0 (SORrm addon)). now apply cltb_sound. - intros. rewrite H1 in H. discriminate. + intros H1. rewrite H1 in H. discriminate. (* PsatzZ *) simpl in *. inv H. unfold eval_nformula. simpl. apply (morph0 (SORrm addon)). Qed. - + @@ -663,8 +666,8 @@ intros l cm H env. unfold check_normalised_formulas in H. revert H. case_eq (eval_Psatz l cm) ; [|discriminate]. -intros nf. intros. -rewrite <- make_conj_impl. intro. +intros nf. intros H H0. +rewrite <- make_conj_impl. intro H1. assert (H1' := make_conj_in _ _ H1). assert (Hnf := @eval_Psatz_Sound _ _ H1' _ _ H). destruct nf. @@ -861,7 +864,7 @@ Proof. set (F := (fun (x : NFormula) (acc : list (list (NFormula * T))) => if check_inconsistent x then acc else ((x, tg) :: nil) :: acc)). set (G := ((fun x : NFormula => eval_nformula env x -> False))). - induction l. + induction l as [|a l IHl]. - compute. tauto. - rewrite make_conj_cons. @@ -896,13 +899,13 @@ Definition cnf_negate {T: Type} (t: Formula C) (tg: T) : cnf NFormula T := Lemma eq0_cnf : forall x, (0 < x -> False) /\ (0 < - x -> False) <-> x == 0. Proof. - split ; intros. + intros x; split ; intros H. + apply (SORle_antisymm sor). * now rewrite (Rle_ngt sor). * rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). setoid_replace (0 - x) with (-x) by ring. tauto. - + split; intro. + + split; intro H0. * rewrite (SORlt_le_neq sor) in H0. apply (proj2 H0). now rewrite H. @@ -918,7 +921,7 @@ Proof. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; repeat rewrite eval_pol_opp; - generalize (eval_pol env e) as x; intro. + generalize (eval_pol env e) as x; intro x. - apply eq0_cnf. - unfold not. tauto. - symmetry. rewrite (Rlt_nge sor). @@ -955,7 +958,7 @@ Proof. intros T env t tg. unfold cnf_normalise. rewrite normalise_sound. - generalize (normalise t) as f;intro. + generalize (normalise t) as f;intro f. destruct (check_inconsistent f) eqn:U. - destruct f as [e op]. assert (US := check_inconsistent_sound _ _ U env). @@ -970,7 +973,7 @@ Proof. intros T env t tg. rewrite normalise_sound. unfold cnf_negate. - generalize (normalise t) as f;intro. + generalize (normalise t) as f;intro f. destruct (check_inconsistent f) eqn:U. - destruct f as [e o]. @@ -983,9 +986,9 @@ Qed. Lemma eval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d). Proof. - intros. - destruct d ; simpl. - generalize (eval_pol env p); intros. + intros env d. + destruct d as [p o]; simpl. + generalize (eval_pol env p); intros r. destruct o ; simpl. apply (Req_em sor r 0). destruct (Req_em sor r 0) ; tauto. @@ -1008,7 +1011,7 @@ Lemma xdenorm_correct : forall p i env, eval_pol (jump i env) p == eval_pexpr env (xdenorm (Pos.succ i) p). Proof. unfold eval_pol. - induction p. + intros p; induction p as [|? p IHp|p2 IHp1 ? p3 IHp2]. simpl. reflexivity. (* Pinj *) simpl. @@ -1037,7 +1040,7 @@ Definition denorm := xdenorm xH. Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p). Proof. unfold denorm. - induction p. + intros p; induction p as [| |? IHp1 ? ? IHp2]. reflexivity. simpl. rewrite Pos.add_1_r. @@ -1092,7 +1095,9 @@ Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop := Lemma eval_pexprSC : forall env s, eval_sexpr env s = eval_pexpr env (map_PExpr s). Proof. unfold eval_pexpr, eval_sexpr. - induction s ; simpl ; try (rewrite IHs1 ; rewrite IHs2) ; try reflexivity. + intros env s; + induction s as [| |? IHs1 ? IHs2|? IHs1 ? IHs2|? IHs1 ? IHs2|? IHs|? IHs ?]; + simpl ; try (rewrite IHs1 ; rewrite IHs2) ; try reflexivity. apply phi_C_of_S. rewrite IHs. reflexivity. rewrite IHs. reflexivity. @@ -1101,7 +1106,7 @@ Qed. (** equality might be (too) strong *) Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f). Proof. - destruct f. + intros env f; destruct f. simpl. repeat rewrite eval_pexprSC. reflexivity. diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index dddced5739..99af214396 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -185,7 +185,7 @@ Section S. | EQ f1 f2 => (eval_f f1) = (eval_f f2) end. Proof. - destruct f ; reflexivity. + intros k f; destruct f ; reflexivity. Qed. End EVAL. @@ -197,23 +197,23 @@ Section S. Definition eiff (k: kind) : rtyp k -> rtyp k -> Prop := if k as k' return rtyp k' -> rtyp k' -> Prop then iff else @eq bool. - Lemma eiff_refl : forall (k: kind) (x : rtyp k), + Lemma eiff_refl (k: kind) (x : rtyp k) : eiff k x x. Proof. destruct k ; simpl; tauto. Qed. - Lemma eiff_sym : forall k (x y : rtyp k), eiff k x y -> eiff k y x. + Lemma eiff_sym k (x y : rtyp k) : eiff k x y -> eiff k y x. Proof. destruct k ; simpl; intros ; intuition. Qed. - Lemma eiff_trans : forall k (x y z : rtyp k), eiff k x y -> eiff k y z -> eiff k x z. + Lemma eiff_trans k (x y z : rtyp k) : eiff k x y -> eiff k y z -> eiff k x z. Proof. destruct k ; simpl; intros ; intuition congruence. Qed. - Lemma hold_eiff : forall (k: kind) (x y : rtyp k), + Lemma hold_eiff (k: kind) (x y : rtyp k) : (hold k x <-> hold k y) <-> eiff k x y. Proof. destruct k ; simpl. @@ -266,7 +266,10 @@ Section S. forall (k: kind)(f : GFormula k), (eiff k (eval_f ev f) (eval_f ev' f)). Proof. - induction f ; simpl. + intros ev ev' H k f; + induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? ? IHf + |? ? IHf1 ? ? IHf2|? ? IHf1 ? IHf2|]; + simpl. - reflexivity. - reflexivity. - reflexivity. @@ -319,7 +322,7 @@ Lemma map_simpl : forall A B f l, @map A B f l = match l with | a :: l=> (f a) :: (@map A B f l) end. Proof. - destruct l ; reflexivity. + intros A B f l; destruct l ; reflexivity. Qed. @@ -469,7 +472,7 @@ Section S. Lemma is_bool_inv : forall {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula TX AF k) res, is_bool f = Some res -> f = if res then TT _ else FF _. Proof. - intros. + intros TX AF k f res H. destruct f ; inversion H; reflexivity. Qed. @@ -689,7 +692,7 @@ Section S. Definition is_X_inv : forall (k: kind) (f: TFormula TX AF k) x, is_X f = Some x -> f = X k x. Proof. - destruct f ; simpl ; try congruence. + intros k f; destruct f ; simpl ; try congruence. Qed. Variable needA : Annot -> bool. @@ -786,7 +789,7 @@ Section S. Lemma if_same : forall {A: Type} (b: bool) (t:A), (if b then t else t) = t. Proof. - destruct b ; reflexivity. + intros A b; destruct b ; reflexivity. Qed. Lemma is_cnf_tt_cnf_ff : @@ -806,14 +809,14 @@ Section S. is_cnf_tt f1 = true -> f1 = cnf_tt. Proof. unfold cnf_tt. - destruct f1 ; simpl ; try congruence. + intros f1; destruct f1 ; simpl ; try congruence. Qed. Lemma is_cnf_ff_inv : forall f1, is_cnf_ff f1 = true -> f1 = cnf_ff. Proof. unfold cnf_ff. - destruct f1 ; simpl ; try congruence. + intros f1 ; destruct f1 as [|c f1] ; simpl ; try congruence. destruct c ; simpl ; try congruence. destruct f1 ; try congruence. reflexivity. @@ -822,7 +825,7 @@ Section S. Lemma if_cnf_tt : forall f, (if is_cnf_tt f then cnf_tt else f) = f. Proof. - intros. + intros f. destruct (is_cnf_tt f) eqn:EQ. apply is_cnf_tt_inv in EQ;auto. reflexivity. @@ -831,7 +834,7 @@ Section S. Lemma or_cnf_opt_cnf_ff : forall f, or_cnf_opt cnf_ff f = f. Proof. - intros. + intros f. unfold or_cnf_opt. rewrite is_cnf_tt_cnf_ff. simpl. @@ -848,7 +851,7 @@ Section S. and_cnf_opt (xcnf pol f1) (xcnf pol f2) = xcnf pol (abs_and f1 f2 (if pol then AND else OR)). Proof. - unfold abs_and; intros. + unfold abs_and; intros k f1 f2 pol. destruct (is_X f1) eqn:EQ1. apply is_X_inv in EQ1. subst. @@ -868,7 +871,7 @@ Section S. or_cnf_opt (xcnf pol f1) (xcnf pol f2) = xcnf pol (abs_or f1 f2 (if pol then OR else AND)). Proof. - unfold abs_or; intros. + unfold abs_or; intros k f1 f2 pol. destruct (is_X f1) eqn:EQ1. apply is_X_inv in EQ1. subst. @@ -889,7 +892,7 @@ Section S. Lemma xcnf_true_mk_arrow_l : forall b o t (f:TFormula TX AF b), xcnf true (mk_arrow o (X b t) f) = xcnf true f. Proof. - destruct o ; simpl; auto. + intros b o; destruct o ; simpl; auto. intros. rewrite or_cnf_opt_cnf_ff. reflexivity. Qed. @@ -907,8 +910,8 @@ Section S. Lemma xcnf_true_mk_arrow_r : forall b o t (f:TFormula TX AF b), xcnf true (mk_arrow o f (X b t)) = xcnf false f. Proof. - destruct o ; simpl; auto. - - intros. + intros b o; destruct o ; simpl; auto. + - intros t f. destruct (is_X f) eqn:EQ. apply is_X_inv in EQ. subst. reflexivity. simpl. @@ -939,7 +942,7 @@ Section S. Lemma and_cnf_opt_cnf_tt : forall f, and_cnf_opt f cnf_tt = f. Proof. - intros. + intros f. unfold and_cnf_opt. simpl. rewrite orb_comm. simpl. @@ -951,7 +954,7 @@ Section S. Lemma is_bool_abst_simpl : forall b (f:TFormula TX AF b), is_bool (abst_simpl f) = is_bool f. Proof. - induction f ; simpl ; auto. + intros b f; induction f ; simpl ; auto. rewrite needA_all. reflexivity. Qed. @@ -959,7 +962,10 @@ Section S. Lemma abst_simpl_correct : forall b (f:TFormula TX AF b) pol, xcnf pol f = xcnf pol (abst_simpl f). Proof. - induction f; simpl;intros; + intros b f; + induction f as [| | | |? ? IHf1 f2 IHf2|? ? IHf1 f2 IHf2 + |? ? IHf|? ? IHf1 ? f2 IHf2|? ? IHf1 f2 IHf2|f1 IHf1 f2 IHf2]; + simpl;intros; unfold mk_and,mk_or,mk_impl, mk_iff; rewrite <- ?IHf; try (rewrite <- !IHf1; rewrite <- !IHf2); @@ -972,11 +978,11 @@ Section S. destruct (is_bool f2); auto. Qed. - Ltac is_X := + Ltac is_X t := match goal with | |-context[is_X ?X] => let f := fresh "EQ" in - destruct (is_X X) eqn:f ; + destruct (is_X X) as [t|] eqn:f ; [apply is_X_inv in f|] end. @@ -995,10 +1001,10 @@ Section S. Proof. unfold or_is_X. intros k f1 f2. - repeat is_X. - exists t ; intuition. + is_X t; is_X t0. exists t ; intuition. exists t ; intuition. + exists t0 ; intuition. congruence. Qed. @@ -1008,8 +1014,8 @@ Section S. | None => mk_iff xcnf pol f1 f2 end = mk_iff xcnf pol f1 f2. Proof. - intros. - destruct (is_bool f2) eqn:EQ; auto. + intros k f1 f2 pol. + destruct (is_bool f2) as [b|] eqn:EQ; auto. apply is_bool_inv in EQ. subst. unfold mk_iff. @@ -1024,7 +1030,7 @@ Section S. (pol : bool), xcnf pol (IFF f1 f2) = xcnf pol (abst_iff abst_form pol f1 f2). Proof. - intros; simpl. + intros k f1 f2 IHf1 IHf2 pol; simpl. assert (D1 :mk_iff xcnf pol f1 f2 = mk_iff xcnf pol (abst_simpl f1) (abst_simpl f2)). { simpl. @@ -1066,7 +1072,7 @@ Section S. (pol : bool), xcnf pol (EQ f1 f2) = xcnf pol (abst_form pol (EQ f1 f2)). Proof. - intros. + intros f1 f2 IHf1 IHf2 pol. change (xcnf pol (IFF f1 f2) = xcnf pol (abst_form pol (EQ f1 f2))). rewrite abst_iff_correct by assumption. simpl. unfold abst_iff, abst_eq. @@ -1080,7 +1086,10 @@ Section S. Lemma abst_form_correct : forall b (f:TFormula TX AF b) pol, xcnf pol f = xcnf pol (abst_form pol f). Proof. - induction f;intros. + intros b f; + induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? f IHf + |? f1 IHf1 o f2 IHf2|? IHf1 ? IHf2|]; + intros pol. - simpl. destruct pol ; reflexivity. - simpl. destruct pol ; reflexivity. - simpl. reflexivity. @@ -1178,14 +1187,14 @@ Section S. Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl. Proof. - induction a' ; simpl. - - intros. - destruct (deduce (fst a) (fst a)). + intros a'; induction a' as [|a a' IHa']; simpl. + - intros a cl H. + destruct (deduce (fst a) (fst a)) as [t|]. destruct (unsat t). congruence. inversion H. reflexivity. inversion H ;reflexivity. - - intros. - destruct (deduce (fst a0) (fst a)). + - intros a0 cl H. + destruct (deduce (fst a0) (fst a)) as [t|]. destruct (unsat t). congruence. destruct (radd_term a0 a') eqn:RADD; try congruence. inversion H. subst. @@ -1201,14 +1210,14 @@ Section S. Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl. Proof. - induction a' ; simpl. - - intros. - destruct (deduce (fst a) (fst a)). + intros a'; induction a' as [|a a' IHa']; simpl. + - intros a cl H. + destruct (deduce (fst a) (fst a)) as [t|]. destruct (unsat t). congruence. inversion H. reflexivity. inversion H ;reflexivity. - - intros. - destruct (deduce (fst a0) (fst a)). + - intros a0 cl H. + destruct (deduce (fst a0) (fst a)) as [t|]. destruct (unsat t). congruence. destruct (add_term a0 a') eqn:RADD; try congruence. inversion H. subst. @@ -1229,7 +1238,7 @@ Section S. unfold xor_clause_cnf. assert (ACC: fst (@nil clause,@nil Annot) = nil). reflexivity. - intros. + intros a f. set (F1:= (fun '(acc, tg) (e : clause) => match ror_clause a e with | inl cl => (cl :: acc, tg) @@ -1243,15 +1252,15 @@ Section S. revert ACC. generalize (@nil clause,@nil Annot). generalize (@nil clause). - induction f ; simpl ; auto. - intros. + induction f as [|a0 f IHf]; simpl ; auto. + intros ? p ?. apply IHf. unfold F1 , F2. destruct p ; simpl in * ; subst. clear. revert a0. - induction a; simpl; auto. - intros. + induction a as [|a a0 IHa]; simpl; auto. + intros a1. destruct (radd_term a a1) eqn:RADD. apply radd_term_term in RADD. rewrite RADD. @@ -1266,14 +1275,14 @@ Section S. fst (ror_clause_cnf a f) = or_clause_cnf a f. Proof. unfold ror_clause_cnf,or_clause_cnf. - destruct a ; auto. + intros a; destruct a ; auto. apply xror_clause_clause. Qed. Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2. Proof. - induction f1 ; simpl ; auto. - intros. + intros f1; induction f1 as [|a f1 IHf1] ; simpl ; auto. + intros f2. specialize (IHf1 f2). destruct(ror_cnf f1 f2). rewrite <- ror_clause_clause. @@ -1286,7 +1295,7 @@ Section S. Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2. Proof. unfold ror_cnf_opt, or_cnf_opt. - intros. + intros f1 f2. destruct (is_cnf_tt f1). - simpl ; auto. - simpl. destruct (is_cnf_tt f2) ; simpl ; auto. @@ -1299,7 +1308,7 @@ Section S. fst (ratom f a) = f. Proof. unfold ratom. - intros. + intros f a. destruct (is_cnf_ff f || is_cnf_tt f); auto. Qed. @@ -1308,7 +1317,7 @@ Section S. (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), forall pol : bool, fst (rxcnf_and rxcnf pol f1 f2) = mk_and xcnf pol f1 f2. Proof. - intros. + intros TX AF k f1 f2 IHf1 IHf2 pol. unfold mk_and, rxcnf_and. specialize (IHf1 pol). specialize (IHf2 pol). @@ -1327,7 +1336,7 @@ Section S. (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), forall pol : bool, fst (rxcnf_or rxcnf pol f1 f2) = mk_or xcnf pol f1 f2. Proof. - intros. + intros TX AF k f1 f2 IHf1 IHf2 pol. unfold rxcnf_or, mk_or. specialize (IHf1 pol). specialize (IHf2 pol). @@ -1346,7 +1355,7 @@ Section S. (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), forall pol : bool, fst (rxcnf_impl rxcnf pol f1 f2) = mk_impl xcnf pol f1 f2. Proof. - intros. + intros TX AF k f1 f2 IHf1 IHf2 pol. unfold rxcnf_impl, mk_impl, mk_or. specialize (IHf1 (negb pol)). specialize (IHf2 pol). @@ -1359,7 +1368,7 @@ Section S. destruct pol;auto. generalize (is_cnf_ff_inv (xcnf (negb true) f1)). destruct (is_cnf_ff (xcnf (negb true) f1)). - + intros. + + intros H. rewrite H by auto. unfold or_cnf_opt. simpl. @@ -1384,18 +1393,18 @@ Section S. (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), forall pol : bool, fst (rxcnf_iff rxcnf pol f1 f2) = mk_iff xcnf pol f1 f2. Proof. - intros. + intros TX AF k f1 f2 IHf1 IHf2 pol. unfold rxcnf_iff. unfold mk_iff. rewrite <- (IHf1 (negb pol)). rewrite <- (IHf1 pol). rewrite <- (IHf2 false). rewrite <- (IHf2 true). - destruct (rxcnf (negb pol) f1). - destruct (rxcnf false f2). - destruct (rxcnf pol f1). - destruct (rxcnf true f2). - destruct (ror_cnf_opt (and_cnf_opt c c0) (and_cnf_opt c1 c2)) eqn:EQ. + destruct (rxcnf (negb pol) f1) as [c ?]. + destruct (rxcnf false f2) as [c0 ?]. + destruct (rxcnf pol f1) as [c1 ?]. + destruct (rxcnf true f2) as [c2 ?]. + destruct (ror_cnf_opt (and_cnf_opt c c0) (and_cnf_opt c1 c2)) as [c3 l3] eqn:EQ. simpl. change c3 with (fst (c3,l3)). rewrite <- EQ. rewrite ror_opt_cnf_cnf. @@ -1405,7 +1414,7 @@ Section S. Lemma rxcnf_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f:TFormula TX AF k) pol, fst (rxcnf pol f) = xcnf pol f. Proof. - induction f ; simpl ; auto. + intros TX AF k f; induction f ; simpl ; auto; intros pol. - destruct pol; simpl ; auto. - destruct pol; simpl ; auto. - destruct pol ; simpl ; auto. @@ -1463,7 +1472,7 @@ Section S. Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y). Proof. unfold and_cnf_opt. - intros. + intros env x y. destruct (is_cnf_ff x) eqn:F1. { apply is_cnf_ff_inv in F1. simpl. subst. @@ -1501,14 +1510,14 @@ Section S. Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl). Proof. - induction cl. + intros env t cl; induction cl as [|a cl IHcl]. - (* BC *) simpl. case_eq (deduce (fst t) (fst t)) ; try tauto. - intros. + intros t0 H. generalize (@deduce_prop _ _ _ H env). case_eq (unsat t0) ; try tauto. - { intros. + { intros H0 ?. generalize (@unsat_prop _ H0 env). unfold eval_clause. rewrite make_conj_cons. @@ -1518,9 +1527,9 @@ Section S. - (* IC *) simpl. case_eq (deduce (fst t) (fst a)); - intros. + intros t0; [intros H|]. generalize (@deduce_prop _ _ _ H env). - case_eq (unsat t0); intros. + case_eq (unsat t0); intros H0 H1. { generalize (@unsat_prop _ H0 env). simpl. @@ -1557,9 +1566,9 @@ Section S. Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') <-> eval_clause env cl \/ eval_clause env cl'. Proof. - induction cl. + intros cl; induction cl as [|a cl IHcl]. - simpl. unfold eval_clause at 2. simpl. tauto. - - intros *. + - intros cl' env. simpl. assert (HH := add_term_correct env a cl'). assert (eval_tt env a \/ ~ eval_tt env a) by (apply no_middle_eval'). @@ -1579,17 +1588,17 @@ Section S. Proof. unfold eval_cnf. unfold or_clause_cnf. - intros until t. + intros env t. set (F := (fun (acc : list clause) (e : clause) => match or_clause t e with | Some cl => cl :: acc | None => acc end)). intro f. - assert ( make_conj (eval_clause env) (fold_left F f nil) <-> (eval_clause env t \/ make_conj (eval_clause env) f) /\ make_conj (eval_clause env) nil). + assert ( make_conj (eval_clause env) (fold_left F f nil) <-> (eval_clause env t \/ make_conj (eval_clause env) f) /\ make_conj (eval_clause env) nil) as H. { generalize (@nil clause) as acc. - induction f. + induction f as [|a f IHf]. - simpl. intros ; tauto. - intros. @@ -1634,7 +1643,7 @@ Section S. Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') <-> (eval_cnf env f) \/ (eval_cnf env f'). Proof. - induction f. + intros env f; induction f as [|a f IHf]. unfold eval_cnf. simpl. tauto. @@ -1652,7 +1661,7 @@ Section S. Lemma or_cnf_opt_correct : forall env f f', eval_cnf env (or_cnf_opt f f') <-> eval_cnf env (or_cnf f f'). Proof. unfold or_cnf_opt. - intros. + intros env f f'. destruct (is_cnf_tt f) eqn:TF. { simpl. apply is_cnf_tt_inv in TF. @@ -1690,7 +1699,7 @@ Section S. Lemma hold_eTT : forall k, hold k (eTT k). Proof. - destruct k ; simpl; auto. + intros k; destruct k ; simpl; auto. Qed. Hint Resolve hold_eTT : tauto. @@ -1698,7 +1707,7 @@ Section S. Lemma hold_eFF : forall k, hold k (eNOT k (eFF k)). Proof. - destruct k ; simpl;auto. + intros k; destruct k ; simpl;auto. Qed. Hint Resolve hold_eFF : tauto. @@ -1706,7 +1715,7 @@ Section S. Lemma hold_eAND : forall k r1 r2, hold k (eAND k r1 r2) <-> (hold k r1 /\ hold k r2). Proof. - destruct k ; simpl. + intros k; destruct k ; simpl. - intros. apply iff_refl. - apply andb_true_iff. Qed. @@ -1714,7 +1723,7 @@ Section S. Lemma hold_eOR : forall k r1 r2, hold k (eOR k r1 r2) <-> (hold k r1 \/ hold k r2). Proof. - destruct k ; simpl. + intros k; destruct k ; simpl. - intros. apply iff_refl. - apply orb_true_iff. Qed. @@ -1722,9 +1731,9 @@ Section S. Lemma hold_eNOT : forall k e, hold k (eNOT k e) <-> not (hold k e). Proof. - destruct k ; simpl. + intros k; destruct k ; simpl. - intros. apply iff_refl. - - intros. unfold is_true. + - intros e. unfold is_true. rewrite negb_true_iff. destruct e ; intuition congruence. Qed. @@ -1732,9 +1741,9 @@ Section S. Lemma hold_eIMPL : forall k e1 e2, hold k (eIMPL k e1 e2) <-> (hold k e1 -> hold k e2). Proof. - destruct k ; simpl. + intros k; destruct k ; simpl. - intros. apply iff_refl. - - intros. + - intros e1 e2. unfold is_true. destruct e1,e2 ; simpl ; intuition congruence. Qed. @@ -1742,9 +1751,9 @@ Section S. Lemma hold_eIFF : forall k e1 e2, hold k (eIFF k e1 e2) <-> (hold k e1 <-> hold k e2). Proof. - destruct k ; simpl. + intros k; destruct k ; simpl. - intros. apply iff_refl. - - intros. + - intros e1 e2. unfold is_true. rewrite eqb_true_iff. destruct e1,e2 ; simpl ; intuition congruence. @@ -1768,7 +1777,7 @@ Section S. eval_cnf env (xcnf pol (IMPL f1 o f2)) -> hold k (eval_f e_rtyp (eval env) (if pol then IMPL f1 o f2 else NOT (IMPL f1 o f2))). Proof. - simpl; intros. unfold mk_impl in H. + simpl; intros k f1 o f2 IHf1 IHf2 pol env H. unfold mk_impl in H. destruct pol. + simpl. rewrite hold_eIMPL. @@ -1810,7 +1819,7 @@ Section S. hold isBool (eIFF isBool e1 e2) <-> e1 = e2. Proof. simpl. - destruct e1,e2 ; simpl ; intuition congruence. + intros e1 e2; destruct e1,e2 ; simpl ; intuition congruence. Qed. @@ -1828,7 +1837,7 @@ Section S. hold k (eval_f e_rtyp (eval env) (if pol then IFF f1 f2 else NOT (IFF f1 f2))). Proof. simpl. - intros. + intros k f1 f2 IHf1 IHf2 pol env H. rewrite mk_iff_is_bool in H. unfold mk_iff in H. destruct pol; @@ -1858,7 +1867,10 @@ Section S. Lemma xcnf_correct : forall (k: kind) (f : @GFormula Term rtyp Annot unit k) pol env, eval_cnf env (xcnf pol f) -> hold k (eval_f e_rtyp (eval env) (if pol then f else NOT f)). Proof. - induction f. + intros k f; + induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? ? IHf + |? ? IHf1 ? ? IHf2|? ? IHf1 f2 IHf2|f1 IHf1 f2 IHf2]; + intros pol env H. - (* TT *) unfold eval_cnf. simpl. @@ -1881,13 +1893,13 @@ Section S. intros. eapply negate_correct ; eauto. - (* AND *) - destruct pol ; simpl. + destruct pol ; simpl in H. + (* pol = true *) intros. rewrite eval_cnf_and_opt in H. unfold and_cnf in H. rewrite eval_cnf_app in H. - destruct H. + destruct H as [H H0]. apply hold_eAND; split. apply (IHf1 _ _ H). apply (IHf2 _ _ H0). @@ -1907,7 +1919,7 @@ Section S. rewrite hold_eNOT. tauto. - (* OR *) - simpl. + simpl in H. destruct pol. + (* pol = true *) intros. unfold mk_or in H. @@ -1947,8 +1959,8 @@ Section S. - (* IMPL *) apply xcnf_impl; auto. - apply xcnf_iff ; auto. - - simpl. - destruct (is_bool f2) eqn:EQ. + - simpl in H. + destruct (is_bool f2) as [b|] eqn:EQ. + apply is_bool_inv in EQ. destruct b; subst; intros; apply IHf1 in H; @@ -1996,17 +2008,17 @@ Section S. Lemma cnf_checker_sound : forall t w, cnf_checker t w = true -> forall env, eval_cnf env t. Proof. unfold eval_cnf. - induction t. + intros t; induction t as [|a t IHt]. (* bc *) simpl. auto. (* ic *) simpl. - destruct w. + intros w; destruct w as [|w ?]. intros ; discriminate. - case_eq (checker a w) ; intros ; try discriminate. + case_eq (checker a w) ; intros H H0 env ** ; try discriminate. generalize (@checker_sound _ _ H env). - generalize (IHt _ H0 env) ; intros. + generalize (IHt _ H0 env) ; intros H1 H2. destruct t. red ; intro. rewrite <- make_conj_impl in H2. @@ -2021,7 +2033,7 @@ Section S. Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f e_rtyp (eval env) t. Proof. unfold tauto_checker. - intros. + intros t w H env. change (eval_f e_rtyp (eval env) t) with (eval_f e_rtyp (eval env) (if true then t else TT isProp)). apply (xcnf_correct t true). eapply cnf_checker_sound ; eauto. @@ -2032,7 +2044,10 @@ Section S. Lemma eval_bf_map : forall T U (fct: T-> U) env (k: kind) (f:BFormula T k) , eval_bf env (map_bformula fct f) = eval_bf (fun b x => env b (fct x)) f. Proof. - induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. + intros T U fct env k f; + induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? ? IHf + |? ? IHf1 ? ? IHf2|? ? IHf1 ? IHf2|? IHf1 ? IHf2]; + simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. rewrite <- IHf. auto. Qed. diff --git a/theories/micromega/ZCoeff.v b/theories/micromega/ZCoeff.v index 4e04adaddb..aaaeb9e118 100644 --- a/theories/micromega/ZCoeff.v +++ b/theories/micromega/ZCoeff.v @@ -121,7 +121,7 @@ Qed. Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x. Proof. -induction x as [x IH | x IH |]; simpl; +intros x; induction x as [x IH | x IH |]; simpl; try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_pos_pos sor); try apply (Rlt_0_1 sor); assumption. Qed. diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index 37eef12381..f6ade67c5f 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -210,7 +210,7 @@ Qed. Lemma eq_iff : forall (P Q : Prop), P = Q -> (P <-> Q). Proof. - intros. + intros P Q H. rewrite H. apply iff_refl. Defined. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index 0e135ba793..9881e73f76 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -139,7 +139,7 @@ Add Zify BinRel Op_pos_le. Lemma eq_pos_inj : forall (x y:positive), x = y <-> Z.pos x = Z.pos y. Proof. - intros. + intros x y. apply (iff_sym (Pos2Z.inj_iff x y)). Qed. @@ -186,7 +186,7 @@ Add Zify UnOp Op_pos_pred. Instance Op_pos_predN : UnOp Pos.pred_N := { TUOp := fun x => x - 1 ; - TUOpInj := ltac: (now destruct x; rewrite N.pos_pred_spec) }. + TUOpInj x := ltac: (now destruct x; rewrite N.pos_pred_spec) }. Add Zify UnOp Op_pos_predN. Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat := @@ -195,7 +195,7 @@ Add Zify UnOp Op_pos_of_succ_nat. Instance Op_pos_of_nat : UnOp Pos.of_nat := { TUOp := fun x => Z.max 1 x ; - TUOpInj := ltac: (now destruct x; + TUOpInj x := ltac: (now destruct x; [|rewrite <- Pos.of_nat_succ, <- (Nat2Z.inj_max 1)]) }. Add Zify UnOp Op_pos_of_nat. @@ -445,7 +445,7 @@ Add Zify UnOp Op_Z_quot2. Lemma of_nat_to_nat_eq : forall x, Z.of_nat (Z.to_nat x) = Z.max 0 x. Proof. - destruct x. + intros x; destruct x. - reflexivity. - rewrite Z2Nat.id. reflexivity. diff --git a/theories/micromega/Ztac.v b/theories/micromega/Ztac.v index 5fb92aba44..a97ea85ceb 100644 --- a/theories/micromega/Ztac.v +++ b/theories/micromega/Ztac.v @@ -26,7 +26,7 @@ Qed. Lemma elim_concl_eq : forall x y, (x < y \/ y < x -> False) -> x = y. Proof. - intros. + intros x y H. destruct (Z_lt_le_dec x y). exfalso. apply H ; auto. destruct (Zle_lt_or_eq y x);auto. @@ -37,7 +37,7 @@ Qed. Lemma elim_concl_le : forall x y, (y < x -> False) -> x <= y. Proof. - intros. + intros x y H. destruct (Z_lt_le_dec y x). exfalso ; auto. auto. @@ -46,7 +46,7 @@ Qed. Lemma elim_concl_lt : forall x y, (y <= x -> False) -> x < y. Proof. - intros. + intros x y H. destruct (Z_lt_le_dec x y). auto. exfalso ; auto. @@ -93,7 +93,7 @@ Qed. Lemma mul_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1*e2. Proof. - intros. + intros e1 e2 H H0. change 0 with (0* e2). apply Zmult_le_compat_r; auto. Qed. diff --git a/theories/setoid_ring/InitialRing.v b/theories/setoid_ring/InitialRing.v index bb98a447dc..c33beaf8cd 100644 --- a/theories/setoid_ring/InitialRing.v +++ b/theories/setoid_ring/InitialRing.v @@ -104,7 +104,7 @@ Section ZMORPHISM. Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ. Proof. constructor. - destruct c;intros;try discriminate. + intros c;destruct c;intros ? H;try discriminate. injection H as [= <-]. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. @@ -119,7 +119,7 @@ Section ZMORPHISM. Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x. Proof. - induction x;simpl. + intros x;induction x as [x IHx|x IHx|];simpl. rewrite IHx;destruct x;simpl;norm. rewrite IHx;destruct x;simpl;norm. rrefl. @@ -128,7 +128,7 @@ Section ZMORPHISM. Lemma ARgen_phiPOS_Psucc : forall x, gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x). Proof. - induction x;simpl;norm. + intros x;induction x as [x IHx|x IHx|];simpl;norm. rewrite IHx;norm. add_push 1;rrefl. Qed. @@ -136,7 +136,8 @@ Section ZMORPHISM. Lemma ARgen_phiPOS_add : forall x y, gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y). Proof. - induction x;destruct y;simpl;norm. + intros x;induction x as [x IHx|x IHx|]; + intros y;destruct y as [y|y|];simpl;norm. rewrite Pos.add_carry_spec. rewrite ARgen_phiPOS_Psucc. rewrite IHx;norm. @@ -152,7 +153,7 @@ Section ZMORPHISM. Lemma ARgen_phiPOS_mult : forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y. Proof. - induction x;intros;simpl;norm. + intros x;induction x as [x IHx|x IHx|];intros;simpl;norm. rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm. rewrite IHx;rrefl. Qed. @@ -169,7 +170,7 @@ Section ZMORPHISM. (*morphisms are extensionally equal*) Lemma same_genZ : forall x, [x] == gen_phiZ1 x. Proof. - destruct x;simpl; try rewrite (same_gen ARth);rrefl. + intros x;destruct x;simpl; try rewrite (same_gen ARth);rrefl. Qed. Lemma gen_Zeqb_ok : forall x y, @@ -198,7 +199,7 @@ Section ZMORPHISM. Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y]. Proof. intros x y; repeat rewrite same_genZ; generalize x y;clear x y. - destruct x, y; simpl; norm. + intros x y;destruct x, y; simpl; norm. apply (ARgen_phiPOS_add ARth). apply gen_phiZ1_pos_sub. rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth). @@ -301,7 +302,7 @@ Section NMORPHISM. Lemma same_genN : forall x, [x] == gen_phiN1 x. Proof. - destruct x;simpl. reflexivity. + intros x;destruct x;simpl. reflexivity. now rewrite (same_gen Rsth Reqe ARth). Qed. @@ -421,7 +422,7 @@ Section NWORDMORPHISM. Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0. Proof. -induction w; simpl; intros; auto. +intros w; induction w as [|a w IHw]; simpl; intros; auto. reflexivity. destruct a. @@ -436,17 +437,17 @@ Qed. Lemma gen_phiNword_cons : forall w n, gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w. -induction w. - destruct n; simpl; norm. +intros w; induction w. + intros n; destruct n; simpl; norm. - intros. + intros n. destruct n; norm. Qed. Lemma gen_phiNword_Nwcons : forall w n, gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w. -destruct w; intros. - destruct n; norm. +intros w; destruct w; intros n0. + destruct n0; norm. unfold Nwcons. rewrite gen_phiNword_cons. @@ -455,13 +456,13 @@ Qed. Lemma gen_phiNword_ok : forall w1 w2, Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2. -induction w1; intros. +intros w1; induction w1 as [|a w1 IHw1]; intros w2 H. simpl. rewrite (gen_phiNword0_ok _ H). reflexivity. rewrite gen_phiNword_cons. - destruct w2. + destruct w2 as [|n w2]. simpl in H. destruct a; try discriminate. rewrite (gen_phiNword0_ok _ H). @@ -481,7 +482,7 @@ Qed. Lemma Nwadd_ok : forall x y, gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y. -induction x; intros. +intros x; induction x as [|n x IHx]; intros y. simpl. norm. @@ -507,7 +508,7 @@ Qed. Lemma Nwscal_ok : forall n x, gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x. -induction x; intros. +intros n x; induction x as [|a x IHx]; intros. norm. simpl Nwscal. @@ -521,7 +522,7 @@ Qed. Lemma Nwmul_ok : forall x y, gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y. -induction x; intros. +intros x; induction x as [|a x IHx]; intros. norm. destruct a. @@ -626,7 +627,7 @@ Qed. Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem. Proof. constructor. - intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst. + intros a b; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst. rewrite Z.mul_comm; rsimpl. Qed. @@ -634,7 +635,7 @@ Qed. Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl. constructor. - intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst. + intros a b; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst. rewrite N.mul_comm; rsimpl. Qed. diff --git a/theories/setoid_ring/Ring.v b/theories/setoid_ring/Ring.v index a66037a956..25b79d1fb2 100644 --- a/theories/setoid_ring/Ring.v +++ b/theories/setoid_ring/Ring.v @@ -17,22 +17,22 @@ Require Export Ring_tac. Lemma BoolTheory : ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)). split; simpl. -destruct x; reflexivity. -destruct x; destruct y; reflexivity. -destruct x; destruct y; destruct z; reflexivity. +intros x; destruct x; reflexivity. +intros x y; destruct x; destruct y; reflexivity. +intros x y z; destruct x; destruct y; destruct z; reflexivity. reflexivity. -destruct x; destruct y; reflexivity. -destruct x; destruct y; reflexivity. -destruct x; destruct y; destruct z; reflexivity. +intros x y; destruct x; destruct y; reflexivity. +intros x y; destruct x; destruct y; reflexivity. +intros x y z; destruct x; destruct y; destruct z; reflexivity. reflexivity. -destruct x; reflexivity. +intros x; destruct x; reflexivity. Qed. Definition bool_eq (b1 b2:bool) := if b1 then b2 else negb b2. Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2. -destruct b1; destruct b2; auto. +intros b1 b2; destruct b1; destruct b2; auto. Qed. Ltac bool_cst t := diff --git a/theories/setoid_ring/Ring_polynom.v b/theories/setoid_ring/Ring_polynom.v index a13b1fc738..0efd82c9bd 100644 --- a/theories/setoid_ring/Ring_polynom.v +++ b/theories/setoid_ring/Ring_polynom.v @@ -559,7 +559,9 @@ Section MakeRingPol. Lemma Peq_ok P P' : (P ?== P') = true -> P === P'. Proof. unfold Pequiv. - revert P';induction P;destruct P';simpl; intros H l; try easy. + revert P';induction P as [|p P IHP|P2 IHP1 p P3 IHP2]; + intros P';destruct P' as [|p0 P'|P'1 p0 P'2];simpl; + intros H l; try easy. - now apply (morph_eq CRmorph). - destruct (Pos.compare_spec p p0); [ subst | easy | easy ]. now rewrite IHP. @@ -643,13 +645,13 @@ Section MakeRingPol. Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c]. Proof. - revert l;induction P;simpl;intros;Esimpl;trivial. + revert l;induction P as [| |P2 IHP1 p P3 IHP2];simpl;intros;Esimpl;trivial. rewrite IHP2;rsimpl. Qed. Lemma PsubC_ok c P l : (PsubC P c)@l == P@l - [c]. Proof. - revert l;induction P;simpl;intros. + revert l;induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros. - Esimpl. - rewrite IHP;rsimpl. - rewrite IHP2;rsimpl. @@ -657,7 +659,7 @@ Section MakeRingPol. Lemma PmulC_aux_ok c P l : (PmulC_aux P c)@l == P@l * [c]. Proof. - revert l;induction P;simpl;intros;Esimpl;trivial. + revert l;induction P as [| |P2 IHP1 p P3 IHP2];simpl;intros;Esimpl;trivial. rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut. Qed. @@ -673,7 +675,7 @@ Section MakeRingPol. Lemma Popp_ok P l : (--P)@l == - P@l. Proof. - revert l;induction P;simpl;intros. + revert l;induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros. - Esimpl. - apply IHP. - rewrite IHP1, IHP2;rsimpl. @@ -686,7 +688,7 @@ Section MakeRingPol. (PaddX Padd P' k P) @ l == P@l + P'@l * (hd l)^k. Proof. intros IHP'. - revert k l. induction P;simpl;intros. + revert k l. induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros. - add_permut. - destruct p; simpl; rewrite ?jump_pred_double; add_permut. @@ -698,8 +700,9 @@ Section MakeRingPol. Lemma Padd_ok P' P l : (P ++ P')@l == P@l + P'@l. Proof. - revert P l; induction P';simpl;intros;Esimpl. - - revert p l; induction P;simpl;intros. + revert P l; induction P' as [|p P' IHP'|P'1 IHP'1 p P'2 IHP'2]; + simpl;intros P l;Esimpl. + - revert p l; induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros p0 l. + Esimpl; add_permut. + destr_pos_sub; intros ->;Esimpl. * now rewrite IHP'. @@ -709,7 +712,7 @@ Section MakeRingPol. * rewrite IHP2;simpl. rsimpl. * rewrite IHP2;simpl. rewrite jump_pred_double. rsimpl. * rewrite IHP'. rsimpl. - - destruct P;simpl. + - destruct P as [|p0 ?|? ? ?];simpl. + Esimpl. add_permut. + destruct p0;simpl;Esimpl; rewrite IHP'2; simpl. * rsimpl. add_permut. @@ -725,14 +728,15 @@ Section MakeRingPol. Lemma Psub_opp P' P : P -- P' === P ++ (--P'). Proof. - revert P; induction P'; simpl; intros. + revert P; induction P' as [|p P' IHP'|P'1 IHP'1 p P'2 IHP'2]; simpl; intros P. - intro l; Esimpl. - - revert p; induction P; simpl; intros; try reflexivity. + - revert p; induction P; simpl; intros p0; try reflexivity. + destr_pos_sub; intros ->; now apply mkPinj_ext. + destruct p0; now apply PX_ext. - - destruct P; simpl; try reflexivity. + - destruct P as [|p0 P|P2 p0 P3]; simpl; try reflexivity. + destruct p0; now apply PX_ext. + destr_pos_sub; intros ->; apply mkPX_ext; auto. + let p1 := match goal with |- PsubX _ _ ?p1 _ === _ => p1 end in revert p1. induction P2; simpl; intros; try reflexivity. destr_pos_sub; intros ->; now apply mkPX_ext. Qed. @@ -746,8 +750,8 @@ Section MakeRingPol. (forall P l, (Pmul P P') @ l == P @ l * P' @ l) -> forall P p l, (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l). Proof. - intros IHP'. - induction P;simpl;intros. + intros IHP' P. + induction P as [|p P IHP|? IHP1 ? ? IHP2];simpl;intros p0 l. - Esimpl; mul_permut. - destr_pos_sub; intros ->;Esimpl. + now rewrite IHP'. @@ -761,10 +765,10 @@ Section MakeRingPol. Lemma Pmul_ok P P' l : (P**P')@l == P@l * P'@l. Proof. - revert P l;induction P';simpl;intros. + revert P l;induction P' as [| |? IHP'1 ? ? IHP'2];simpl;intros P l. - apply PmulC_ok. - apply PmulI_ok;trivial. - - destruct P. + - destruct P as [|p0|]. + rewrite (ARmul_comm ARth). Esimpl. + Esimpl. f_equiv. rewrite IHP'1; Esimpl. destruct p0;rewrite IHP'2;Esimpl. @@ -821,7 +825,8 @@ Section MakeRingPol. P@l == Q@l + [c] * M@@l * R@l. Proof. destruct cM as (c,M). revert M l. - induction P; destruct M; intros l; simpl; auto; + induction P as [c0|p P ?|P2 ? ? P3 ?]; intros M; destruct M; intros l; + simpl; auto; try (case ceqb_spec; intro He); try (case Pos.compare_spec; intros He); rewrite ?He; @@ -858,7 +863,7 @@ Section MakeRingPol. [fst cM1] * (snd cM1)@@l == P2@l -> P1@l == (PNSubst1 P1 cM1 P2 n)@l. Proof. - revert P1. induction n; simpl; intros P1; + revert P1. induction n as [|n IHn]; simpl; intros P1; generalize (POneSubst_ok P1 cM1 P2); destruct POneSubst; intros; rewrite <- ?IHn; auto; reflexivity. Qed. @@ -890,7 +895,7 @@ Section MakeRingPol. Lemma PSubstL_ok n LM1 P1 P2 l : PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l. Proof. - revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. + revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros P3 H **. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. @@ -900,7 +905,7 @@ Section MakeRingPol. Lemma PNSubstL_ok m n LM1 P1 l : MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l. Proof. - revert LM1 P1. induction m; simpl; intros; + revert LM1 P1. induction m as [|m IHm]; simpl; intros LM1 P2 H; assert (H' := PSubstL_ok n LM1 P2); destruct PSubstL; auto; try reflexivity. rewrite <- IHm; auto. @@ -979,7 +984,8 @@ Section POWER. forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l. Proof. intros subst_l_ok res P p. revert res. - induction p;simpl;intros; rewrite ?subst_l_ok, ?Pmul_ok, ?IHp; + induction p as [p IHp|p IHp|];simpl;intros; + rewrite ?subst_l_ok, ?Pmul_ok, ?IHp; mul_permut. Qed. @@ -987,7 +993,7 @@ Section POWER. (forall P, subst_l P@l == P@l) -> forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l. Proof. - destruct n;simpl. + intros ? P n; destruct n;simpl. - reflexivity. - rewrite Ppow_pos_ok by trivial. Esimpl. Qed. @@ -1057,8 +1063,9 @@ Section POWER. PEeval l pe == (norm_aux pe)@l. Proof. intros. - induction pe; cbn. - - now rewrite (morph0 CRmorph). + induction pe as [| |c|p|pe1 IHpe1 pe2 IHpe2|? IHpe1 ? IHpe2|? IHpe1 ? IHpe2 + |? IHpe|? IHpe n0]; cbn. + - now rewrite (morph0 CRmorph). - now rewrite (morph1 CRmorph). - reflexivity. - apply mkX_ok. @@ -1071,8 +1078,9 @@ Section POWER. - rewrite IHpe1, IHpe2. now rewrite Pmul_ok. - rewrite IHpe. Esimpl. - rewrite Ppow_N_ok by reflexivity. - rewrite (rpow_pow_N pow_th). destruct n0; simpl; Esimpl. - induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. + rewrite (rpow_pow_N pow_th). destruct n0 as [|p]; simpl; Esimpl. + induction p as [p IHp|p IHp|];simpl; + now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. Qed. Lemma norm_subst_spec : @@ -1125,7 +1133,7 @@ Section POWER. Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m -> forall l, [fst m] * Mphi l (snd m) == P@l. Proof. - induction P;simpl;intros;Esimpl. + intros P; induction P as [c|p P IHP|P2 IHP1 ? P3 ?];simpl;intros m H l;Esimpl. assert (H1 := (morph_eq CRmorph) c cO). destruct (c ?=! cO). discriminate. @@ -1142,7 +1150,7 @@ Section POWER. end with (P3 ?== P0). assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). - case_eq (mon_of_pol P2);try intros (cc, pp); intros. + case_eq (mon_of_pol P2);try intros (cc, pp); intros H0 H1. inversion H1. simpl. rewrite mkVmon_ok;simpl. @@ -1155,16 +1163,16 @@ Section POWER. Lemma interp_PElist_ok : forall l lpe, interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l. Proof. - induction lpe;simpl. trivial. - destruct a;simpl;intros. + intros l lpe; induction lpe as [|a lpe IHlpe];simpl. trivial. + destruct a as [p p0];simpl;intros H. assert (HH:=mon_of_pol_ok (norm_subst 0 nil p)); destruct (mon_of_pol (norm_subst 0 nil p)). split. rewrite <- norm_subst_spec by exact I. - destruct lpe;try destruct H;rewrite <- H; + destruct lpe;try destruct H as [H H0];rewrite <- H; rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial. - apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0. - apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0. + apply IHlpe. destruct lpe;simpl;trivial. destruct H as [H H0]. exact H0. + apply IHlpe. destruct lpe;simpl;trivial. destruct H as [H H0]. exact H0. Qed. Lemma norm_subst_ok : forall n l lpe pe, @@ -1180,7 +1188,7 @@ Section POWER. norm_subst n lmp pe1 ?== norm_subst n lmp pe2) = true -> PEeval l pe1 == PEeval l pe2. Proof. - simpl;intros. + simpl;intros n l lpe pe1 pe2 **. do 2 (rewrite (norm_subst_ok n l lpe);trivial). apply Peq_ok;trivial. Qed. @@ -1285,36 +1293,36 @@ Section POWER. Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm. Proof. - induction lm;intros;simpl;Esimpl. + intros lm; induction lm as [|a lm IHlm];intros;simpl;Esimpl. destruct a as (x,p);Esimpl. rewrite IHlm. rewrite mkmult_pow_spec. Esimpl. Qed. Lemma mkmult1_ok : forall lm, mkmult1 lm == r_list_pow lm. Proof. - destruct lm;simpl;Esimpl. + intros lm; destruct lm as [|p lm];simpl;Esimpl. destruct p. rewrite mkmult_rec_ok;rewrite mkpow_spec;Esimpl. Qed. Lemma mkmultm1_ok : forall lm, mkmultm1 lm == - r_list_pow lm. Proof. - destruct lm;simpl;Esimpl. + intros lm; destruct lm as [|p lm];simpl;Esimpl. destruct p;rewrite mkmult_rec_ok. rewrite mkopp_pow_spec;Esimpl. Qed. Lemma r_list_pow_rev : forall l, r_list_pow (rev' l) == r_list_pow l. Proof. assert - (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l). - induction l;intros;simpl;Esimpl. - destruct a;rewrite IHl;Esimpl. + (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l) as H. + intros l; induction l as [|a l IHl];intros;simpl;Esimpl. + destruct a as [r p];rewrite IHl;Esimpl. rewrite (ARmul_comm ARth (pow_pos rmul r p)). reflexivity. intros;unfold rev'. rewrite H;simpl;Esimpl. Qed. Lemma mkmult_c_pos_ok : forall c lm, mkmult_c_pos c lm == [c]* r_list_pow lm. Proof. - intros;unfold mkmult_c_pos;simpl. + intros c lm;unfold mkmult_c_pos;simpl. assert (H := (morph_eq CRmorph) c cI). rewrite <- r_list_pow_rev; destruct (c ?=! cI). rewrite H;trivial;Esimpl. @@ -1323,8 +1331,8 @@ Section POWER. Lemma mkmult_c_ok : forall c lm, mkmult_c c lm == [c] * r_list_pow lm. Proof. - intros;unfold mkmult_c;simpl. - case_eq (get_sign c);intros. + intros c lm;unfold mkmult_c;simpl. + case_eq (get_sign c);intros c0; try intros H. assert (H1 := (morph_eq CRmorph) c0 cI). destruct (c0 ?=! cI). rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H)). Esimpl. rewrite H1;trivial. @@ -1336,8 +1344,8 @@ Qed. Lemma mkadd_mult_ok : forall rP c lm, mkadd_mult rP c lm == rP + [c]*r_list_pow lm. Proof. - intros;unfold mkadd_mult. - case_eq (get_sign c);intros. + intros rP c lm;unfold mkadd_mult. + case_eq (get_sign c);intros c0; try intros H. rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H));Esimpl. rewrite mkmult_c_pos_ok;Esimpl. rewrite mkmult_c_pos_ok;Esimpl. @@ -1346,13 +1354,13 @@ Qed. Lemma add_pow_list_ok : forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l. Proof. - destruct n;simpl;intros;Esimpl. + intros r n; destruct n;simpl;intros;Esimpl. Qed. Lemma add_mult_dev_ok : forall P rP fv n lm, add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd fv) n * r_list_pow lm. Proof. - induction P;simpl;intros. + intros P; induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros rP fv n lm. rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. change (match P3 with @@ -1377,7 +1385,7 @@ Qed. Lemma mult_dev_ok : forall P fv n lm, mult_dev P fv n lm == P@fv * pow_N rI rmul (hd fv) n * r_list_pow lm. Proof. - induction P;simpl;intros;Esimpl. + intros P; induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros fv n lm;Esimpl. rewrite mkmult_c_ok;rewrite add_pow_list_ok;Esimpl. rewrite IHP. simpl;rewrite add_pow_list_ok;Esimpl. change (match P3 with @@ -1463,7 +1471,7 @@ Qed. Lemma mkmult_pow_ok p r x : mkmult_pow r x p == r * x^p. Proof. - revert r; induction p;intros;simpl;Esimpl;rewrite !IHp;Esimpl. + revert r; induction p as [p IHp|p IHp|];intros;simpl;Esimpl;rewrite !IHp;Esimpl. Qed. Lemma mkpow_ok p x : mkpow x p == x^p. |