diff options
| -rw-r--r-- | src/Util/Bool.v | 34 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 16 |
2 files changed, 28 insertions, 22 deletions
diff --git a/src/Util/Bool.v b/src/Util/Bool.v index 6aa8260af..d15a538cf 100644 --- a/src/Util/Bool.v +++ b/src/Util/Bool.v @@ -61,17 +61,23 @@ Qed. Definition andb_prop : forall a b : bool, a && b = true -> a = true /\ b = true. (* transparent version *) Proof. destruct a, b; simpl; split; try reflexivity; assumption. Defined. -Ltac split_andb := - repeat match goal with - | [ H : andb _ _ = true |- _ ] => apply andb_prop in H; destruct H - | [ H : is_true (andb ?x ?y) |- _ ] - => apply andb_prop in H; - change (is_true x /\ is_true y) in H; - destruct H - | [ H : context[andb ?x ?y = true] |- _ ] - => rewrite (Bool.andb_true_iff x y) in H - | [ H : context[is_true (andb ?x ?y)] |- _ ] - => change (is_true (andb x y)) with (andb x y = true) in H; - rewrite Bool.andb_true_iff in H; - change (x = true /\ y = true) with (is_true x /\ is_true y) in H - end. +Ltac split_andb_step := + match goal with + | [ H : andb _ _ = true |- _ ] => apply andb_prop in H; destruct H + | [ H : is_true (andb ?x ?y) |- _ ] + => apply andb_prop in H; + change (is_true x /\ is_true y) in H; + destruct H + end. +Ltac split_andb := repeat split_andb_step. +Ltac split_andb_in_context_step := + match goal with + | _ => split_andb_step + | [ H : context[andb ?x ?y = true] |- _ ] + => rewrite (Bool.andb_true_iff x y) in H + | [ H : context[is_true (andb ?x ?y)] |- _ ] + => change (is_true (andb x y)) with (andb x y = true) in H; + rewrite Bool.andb_true_iff in H; + change (x = true /\ y = true) with (is_true x /\ is_true y) in H + end. +Ltac split_andb_in_context := repeat split_andb_in_context_step. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index a9dcde3d9..07e9af549 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1170,7 +1170,7 @@ Module Z. refine (proj1 (@reflect_iff_gen _ _ lem b') _); cbv beta iota. - Ltac ltb_to_lt'_hyps_step := + Ltac ltb_to_lt_hyps_step := match goal with | [ H : (?x <? ?y) = ?b |- _ ] => ltb_to_lt_with_hyp H (Zlt_cases x y) @@ -1183,7 +1183,7 @@ Module Z. | [ H : (?x =? ?y) = ?b |- _ ] => ltb_to_lt_with_hyp H (eqb_cases x y) end. - Ltac ltb_to_lt'_goal_step := + Ltac ltb_to_lt_goal_step := match goal with | [ |- (?x <? ?y) = ?b ] => ltb_to_lt_in_goal b (Z.ltb_spec0 x y) @@ -1196,13 +1196,13 @@ Module Z. | [ |- (?x =? ?y) = ?b ] => ltb_to_lt_in_goal b (Z.eqb_spec x y) end. - Ltac ltb_to_lt'_step := - first [ ltb_to_lt'_hyps_step - | ltb_to_lt'_goal_step ]. - Ltac ltb_to_lt' := repeat ltb_to_lt'_step. + Ltac ltb_to_lt_step := + first [ ltb_to_lt_hyps_step + | ltb_to_lt_goal_step ]. + Ltac ltb_to_lt := repeat ltb_to_lt_step. Section R_Rb. - Local Ltac t := intros ? ? []; split; intro; ltb_to_lt'; omega. + Local Ltac t := intros ? ? []; split; intro; ltb_to_lt; omega. Local Notation R_Rb Rb R nR := (forall x y b, Rb x y = b <-> if b then R x y else nR x y). Lemma ltb_lt_iff : R_Rb Z.ltb Z.lt Z.ge. Proof. t. Qed. Lemma leb_le_iff : R_Rb Z.leb Z.le Z.gt. Proof. t. Qed. @@ -1211,7 +1211,7 @@ Module Z. Lemma eqb_eq_iff : R_Rb Z.eqb (@Logic.eq Z) (fun x y => x <> y). Proof. t. Qed. End R_Rb. Hint Rewrite ltb_lt_iff leb_le_iff gtb_gt_iff geb_ge_iff eqb_eq_iff : ltb_to_lt. - Ltac ltb_to_lt := + Ltac ltb_to_lt_in_context := repeat autorewrite with ltb_to_lt in *; cbv beta iota in *. |