diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-19 16:20:47 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-19 16:20:47 -0500 |
commit | d71f9e327bae41e895b4523eb4ac2228eecb05ab (patch) | |
tree | 577fd1450a19fc9c29b30811944fb221b4038797 /src/Util | |
parent | cded6731f79a66018d3660017bda7a284aedf50c (diff) |
Add nat_beq_to_eq
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/NatUtil.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 027fd28b1..fd2102b23 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -59,6 +59,24 @@ Tactic Notation "omega" := coq_omega. Tactic Notation "omega" "*" := omega_with_min_max_case. Tactic Notation "omega" "**" := omega_with_min_max. +Lemma nat_beq_false_iff x y : nat_beq x y = false <-> x <> y. +Proof. + split; intro H; repeat intro; subst. + { erewrite internal_nat_dec_lb in H by reflexivity; congruence. } + { destruct (nat_beq x y) eqn:H'; [ | reflexivity ]. + apply internal_nat_dec_bl in H'; subst; congruence. } +Qed. + +Ltac nat_beq_to_eq := + repeat match goal with + | [ H : nat_beq _ _ = true |- _ ] => apply internal_nat_dec_bl in H + | [ H : is_true (nat_beq _ _) = true |- _ ] => apply internal_nat_dec_bl in H + | [ |- nat_beq _ _ = true ] => apply internal_nat_dec_lb + | [ |- is_true (nat_beq _ _) ] => apply internal_nat_dec_lb + | [ H : nat_beq _ _ = false |- _ ] => apply nat_beq_false_iff in H + | [ |- nat_beq _ _ = false ] => apply nat_beq_false_iff + end. + Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1. Proof. intros. |