diff options
| author | letouzey | 2011-05-05 15:13:04 +0000 |
|---|---|---|
| committer | letouzey | 2011-05-05 15:13:04 +0000 |
| commit | 959543f6f899f0384394f9770abbf17649f69b81 (patch) | |
| tree | 46dc4791f1799a3b2095bec6d887d9aa54f42ad3 /plugins/setoid_ring/Ring2_initial.v | |
| parent | d2bd5d87d23d443f6e41496bdfe5f8e82d675634 (diff) | |
BinInt: Z.add become the alternative Z.add'
It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub.
Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14107 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring/Ring2_initial.v')
| -rw-r--r-- | plugins/setoid_ring/Ring2_initial.v | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ring2_initial.v index f94ad9b0f5..7c5631d4ee 100644 --- a/plugins/setoid_ring/Ring2_initial.v +++ b/plugins/setoid_ring/Ring2_initial.v @@ -146,15 +146,11 @@ Ltac rsimpl := simpl; set_ring_notations. Qed. Lemma gen_phiZ1_add_pos_neg : forall x y, - gen_phiZ1 - match (x ?= y)%positive with - | Eq => Z0 - | Lt => Zneg (y - x) - | Gt => Zpos (x - y) - end + gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y. Proof. intros x y. + rewrite Z.pos_sub_spec. assert (H0 := Pminus_mask_Gt x y). unfold Pos.gt in H0. assert (H1 := Pminus_mask_Gt y x). unfold Pos.gt in H1. rewrite Pos.compare_antisym in H1. @@ -181,11 +177,8 @@ Ltac rsimpl := simpl; set_ring_notations. induction x;destruct y;simpl;norm. apply ARgen_phiPOS_add. apply gen_phiZ1_add_pos_neg. - replace Eq with (CompOpp Eq);trivial. - rewrite Pos.compare_antisym;simpl. - ring_rewrite match_compOpp. - ring_rewrite ring_add_comm. - apply gen_phiZ1_add_pos_neg. + rewrite gen_phiZ1_add_pos_neg. + ring_rewrite ring_add_comm. norm. ring_rewrite ARgen_phiPOS_add; norm. Qed. |