diff options
-rw-r--r-- | tactics/tactics.ml | 19 | ||||
-rw-r--r-- | theories/QArith/Qreduction.v | 6 | ||||
-rw-r--r-- | theories/ZArith/Zcomplements.v | 14 |
3 files changed, 16 insertions, 23 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 808f53892..f66c18822 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1850,6 +1850,9 @@ let rewrite_hyp assert_style l2r id = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq c = tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in + if assert_style then + rew_on l2r allHypsAndConcl + else Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_type_of gl in @@ -1863,26 +1866,16 @@ let rewrite_hyp assert_style l2r id = else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then subst_on l2r (destVar rhs) lhs else -(* - if assert_style then - rew_on l2r allHypsAndConcl - else -*) - (* Tacticals.New.tclTHEN *) (rew_on l2r onConcl) (*(Proofview.V82.tactic (tclTRY (clear [id]))) *) + Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) | Some (hdcncl,[c]) -> let l2r = not l2r in (* equality of the form eq_true *) if isVar c then Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c)) else - rew_on l2r allHypsAndConcl -(* - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))*) + Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) | _ -> - if assert_style then - rew_on l2r allHypsAndConcl - else - Tacticals.New.tclZEROMSG (str"Cannot find a known equation.") + Tacticals.New.tclZEROMSG (str"Cannot find a known equation.") end let rec prepare_naming loc = function diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 7d8ed5275..2aac617eb 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -46,12 +46,12 @@ Proof. generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). - simpl. intros <- Hg1 Hg2 (Hg3,Hg4). clear H0. - assert (Hg0 : g <> 0). (intro; now subst g). Show Proof. + simpl. intros <- Hg1 Hg2 (Hg3,Hg4). + assert (Hg0 : g <> 0) by (intro; now subst g). generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)). destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). - simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). clear H0. + simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). assert (Hg'0 : g' <> 0) by (intro; now subst g'). elim (rel_prime_cross_prod aa bb cc dd). diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index be975e882..99b631905 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -54,17 +54,17 @@ Theorem Z_lt_abs_rec : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z * P (- z)). - enough (H:Q (Z.abs p)) by admit. -(* (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).*) + enough (H:Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). apply (Z_lt_rec Q); auto with zarith. subst Q; intros x H. split; apply HP. - rewrite Z.abs_eq; auto; intros. destruct (H (Z.abs m)); auto with zarith. - (* destruct (Zabs_dec m) as [-> | ->]; trivial. *) admit. + destruct (Zabs_dec m) as [-> | ->]; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial; admit. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. Theorem Z_lt_abs_induction : @@ -74,8 +74,8 @@ 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 admit. -(* (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).*) + enough (Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). apply (Z_lt_induction Q); auto with zarith. subst Q; intros. split; apply HP. @@ -84,7 +84,7 @@ Proof. elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial; admit. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. (** To do case analysis over the sign of [z] *) |