diff options
Diffstat (limited to 'theories/Numbers')
25 files changed, 2670 insertions, 1554 deletions
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 7c846571a7..c203c178f5 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -17,7 +17,7 @@ the [Decimal.int] representation. When working with numbers with thousands of digits and more, conversion from/to [Decimal.int] can become significantly slow. If that becomes a problem for your - development, this file provides some alternative [Numeral + development, this file provides some alternative [Number Notation] commands that use [Z] as bridge type. To enable these commands, just be sure to [Require] this file after other files defining numeral notations. diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v index dd361562ba..87a9f704cd 100644 --- a/theories/Numbers/DecimalFacts.v +++ b/theories/Numbers/DecimalFacts.v @@ -10,175 +10,425 @@ (** * DecimalFacts : some facts about Decimal numbers *) -Require Import Decimal Arith. +Require Import Decimal Arith ZArith. + +Variant digits := d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9. + +Fixpoint to_list (u : uint) : list digits := + match u with + | Nil => nil + | D0 u => cons d0 (to_list u) + | D1 u => cons d1 (to_list u) + | D2 u => cons d2 (to_list u) + | D3 u => cons d3 (to_list u) + | D4 u => cons d4 (to_list u) + | D5 u => cons d5 (to_list u) + | D6 u => cons d6 (to_list u) + | D7 u => cons d7 (to_list u) + | D8 u => cons d8 (to_list u) + | D9 u => cons d9 (to_list u) + end. -Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }. -Proof. - decide equality. -Defined. +Fixpoint of_list (l : list digits) : uint := + match l with + | nil => Nil + | cons d0 l => D0 (of_list l) + | cons d1 l => D1 (of_list l) + | cons d2 l => D2 (of_list l) + | cons d3 l => D3 (of_list l) + | cons d4 l => D4 (of_list l) + | cons d5 l => D5 (of_list l) + | cons d6 l => D6 (of_list l) + | cons d7 l => D7 (of_list l) + | cons d8 l => D8 (of_list l) + | cons d9 l => D9 (of_list l) + end. -Lemma rev_revapp d d' : - rev (revapp d d') = revapp d' d. +Lemma of_list_to_list u : of_list (to_list u) = u. +Proof. now induction u; [|simpl; rewrite IHu..]. Qed. + +Lemma to_list_of_list l : to_list (of_list l) = l. +Proof. now induction l as [|h t IHl]; [|case h; simpl; rewrite IHl]. Qed. + +Lemma to_list_inj u u' : to_list u = to_list u' -> u = u'. Proof. - revert d'. induction d; simpl; intros; now rewrite ?IHd. + now intro H; rewrite <-(of_list_to_list u), <-(of_list_to_list u'), H. Qed. -Lemma rev_rev d : rev (rev d) = d. +Lemma of_list_inj u u' : of_list u = of_list u' -> u = u'. Proof. - apply rev_revapp. + now intro H; rewrite <-(to_list_of_list u), <-(to_list_of_list u'), H. Qed. -Lemma revapp_rev_nil d : revapp (rev d) Nil = d. -Proof. now fold (rev (rev d)); rewrite rev_rev. Qed. +Lemma nb_digits_spec u : nb_digits u = length (to_list u). +Proof. now induction u; [|simpl; rewrite IHu..]. Qed. -Lemma app_nil_r d : app d Nil = d. -Proof. now unfold app; rewrite revapp_rev_nil. Qed. +Fixpoint lnzhead l := + match l with + | nil => nil + | cons d l' => + match d with + | d0 => lnzhead l' + | _ => l + end + end. -Lemma app_int_nil_r d : app_int d Nil = d. -Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed. +Lemma nzhead_spec u : to_list (nzhead u) = lnzhead (to_list u). +Proof. now induction u; [|simpl; rewrite IHu|..]. Qed. + +Definition lzero := cons d0 nil. + +Definition lunorm l := + match lnzhead l with + | nil => lzero + | d => d + end. + +Lemma unorm_spec u : to_list (unorm u) = lunorm (to_list u). +Proof. now unfold unorm, lunorm; rewrite <-nzhead_spec; case (nzhead u). Qed. -Lemma revapp_revapp_1 d d' d'' : - nb_digits d <= 1 -> - revapp (revapp d d') d'' = revapp d' (revapp d d''). +Lemma revapp_spec d d' : + to_list (revapp d d') = List.rev_append (to_list d) (to_list d'). +Proof. now revert d'; induction d; intro d'; [|simpl; rewrite IHd..]. Qed. + +Lemma rev_spec d : to_list (rev d) = List.rev (to_list d). +Proof. now unfold rev; rewrite revapp_spec, List.rev_alt; simpl. Qed. + +Lemma app_spec d d' : + to_list (app d d') = Datatypes.app (to_list d) (to_list d'). Proof. - now case d; clear d; intro d; - [|case d; clear d; intro d; - [|simpl; case nb_digits; [|intros n]; intros Hn; exfalso; - [apply (Nat.nle_succ_diag_l _ Hn)| - apply (Nat.nle_succ_0 _ (le_S_n _ _ Hn))]..]..]. + unfold app. + now rewrite revapp_spec, List.rev_append_rev, rev_spec, List.rev_involutive. Qed. -Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d. -Proof. now case d; [|intros d' _; apply Nat.lt_0_succ..]. Qed. +Definition lnztail l := + let fix aux l_rev := + match l_rev with + | cons d0 l_rev => let (r, n) := aux l_rev in pair r (S n) + | _ => pair l_rev O + end in + let (r, n) := aux (List.rev l) in pair (List.rev r) n. -Lemma nb_digits_revapp d d' : - nb_digits (revapp d d') = nb_digits d + nb_digits d'. +Lemma nztail_spec d : + let (r, n) := nztail d in + let (r', n') := lnztail (to_list d) in + to_list r = r' /\ n = n'. Proof. - now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..]. + unfold nztail, lnztail. + set (f := fix aux d_rev := match d_rev with + | D0 d_rev => let (r, n) := aux d_rev in (r, S n) + | _ => (d_rev, 0) end). + set (f' := fix aux (l_rev : list digits) : list digits * nat := + match l_rev with + | cons d0 l_rev => let (r, n) := aux l_rev in (r, S n) + | _ => (l_rev, 0) + end). + rewrite <-(of_list_to_list (rev d)), rev_spec. + induction (List.rev _) as [|h t IHl]; [now simpl|]. + case h; simpl; [|now rewrite rev_spec; simpl; rewrite to_list_of_list..]. + now revert IHl; case f; intros r n; case f'; intros r' n' [-> ->]. Qed. -Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u. -Proof. now unfold rev; rewrite nb_digits_revapp. Qed. +Lemma del_head_spec_0 d : del_head 0 d = d. +Proof. now simpl. Qed. -Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u. -Proof. now induction u; [|apply le_S|..]. Qed. +Lemma del_head_spec_small n d : + n <= length (to_list d) -> to_list (del_head n d) = List.skipn n (to_list d). +Proof. + revert d; induction n as [|n IHn]; intro d; [now simpl|]. + now case d; [|intros d' H; apply IHn, le_S_n..]. +Qed. -Lemma del_head_nb_digits (u:uint) : del_head (nb_digits u) u = Nil. -Proof. now induction u. Qed. +Lemma del_head_spec_large n d : length (to_list d) < n -> del_head n d = zero. +Proof. + revert d; induction n; intro d; [now case d|]. + now case d; [|intro d'; simpl; intro H; rewrite (IHn _ (lt_S_n _ _ H))..]. +Qed. -Lemma nb_digits_del_head n u : - n <= nb_digits u -> nb_digits (del_head n u) = nb_digits u - n. +Lemma nb_digits_0 d : nb_digits d = 0 -> d = Nil. Proof. - revert u; induction n; intros u; [now rewrite Nat.sub_0_r|]. - now case u; clear u; intro u; [|intro Hn; apply IHn, le_S_n..]. + rewrite nb_digits_spec, <-(of_list_to_list d). + now case (to_list d) as [|h t]; [|rewrite to_list_of_list]. Qed. +Lemma nb_digits_n0 d : nb_digits d <> 0 -> d <> Nil. +Proof. now case d; [|intros u _..]. Qed. + Lemma nb_digits_iter_D0 n d : nb_digits (Nat.iter n D0 d) = n + nb_digits d. Proof. now induction n; simpl; [|rewrite IHn]. Qed. -Fixpoint nth n u := - match n with - | O => - match u with - | Nil => Nil - | D0 d => D0 Nil - | D1 d => D1 Nil - | D2 d => D2 Nil - | D3 d => D3 Nil - | D4 d => D4 Nil - | D5 d => D5 Nil - | D6 d => D6 Nil - | D7 d => D7 Nil - | D8 d => D8 Nil - | D9 d => D9 Nil - end - | S n => - match u with - | Nil => Nil - | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => - nth n d - end - end. +Lemma length_lnzhead l : length (lnzhead l) <= length l. +Proof. now induction l as [|h t IHl]; [|case h; [apply le_S|..]]. Qed. + +Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u. +Proof. now induction u; [|apply le_S|..]. Qed. + +Lemma unorm_nzhead u : nzhead u <> Nil -> unorm u = nzhead u. +Proof. now unfold unorm; case nzhead. Qed. -Lemma nb_digits_nth n u : nb_digits (nth n u) <= 1. +Lemma nb_digits_unorm u : u <> Nil -> nb_digits (unorm u) <= nb_digits u. Proof. - revert u; induction n. - - now intro u; case u; [apply Nat.le_0_1|..]. - - intro u; case u; [apply Nat.le_0_1|intro u'; apply IHn..]. + intro Hu; case (uint_eq_dec (nzhead u) Nil). + { unfold unorm; intros ->; simpl. + now revert Hu; case u; [|intros u' _; apply le_n_S, Nat.le_0_l..]. } + intro H; rewrite (unorm_nzhead _ H); apply nb_digits_nzhead. Qed. -Lemma del_head_nth n u : - n < nb_digits u -> - del_head n u = revapp (nth n u) (del_head (S n) u). -Proof. - revert u; induction n; intro u; [now case u|]. - now case u; [|intro u'; intro H; apply IHn, le_S_n..]. -Qed. - -Lemma nth_revapp_r n d d' : - nb_digits d <= n -> - nth n (revapp d d') = nth (n - nb_digits d) d'. -Proof. - revert d d'; induction n; intro d. - - now case d; intro d'; - [case d'|intros d'' H; exfalso; revert H; apply Nat.nle_succ_0..]. - - now induction d; - [intro d'; case d'| - intros d' H; - simpl revapp; rewrite IHd; [|now apply le_Sn_le]; - rewrite Nat.sub_succ_l; [|now apply le_S_n]; - simpl; rewrite <-(IHn _ _ (le_S_n _ _ H))..]. -Qed. - -Lemma nth_revapp_l n d d' : - n < nb_digits d -> - nth n (revapp d d') = nth (nb_digits d - n - 1) d. -Proof. - revert d d'; induction n; intro d. - - rewrite Nat.sub_0_r. - now induction d; - [|intros d' _; simpl revapp; - revert IHd; case d; clear d; [|intro d..]; intro IHd; - [|rewrite IHd; [simpl nb_digits; rewrite (Nat.sub_succ_l _ (S _))|]; - [|apply le_n_S, Nat.le_0_l..]..]..]. - - now induction d; - [|intros d' H; - simpl revapp; simpl nb_digits; - simpl in H; generalize (lt_S_n _ _ H); clear H; intro H; - case (le_lt_eq_dec _ _ H); clear H; intro H; - [rewrite (IHd _ H), Nat.sub_succ_l; - [rewrite Nat.sub_succ_l; [|apply Nat.le_add_le_sub_r]| - apply le_Sn_le]| - rewrite nth_revapp_r; rewrite <-H; - [rewrite Nat.sub_succ, Nat.sub_succ_l; [rewrite !Nat.sub_diag|]|]]..]. -Qed. - -Lemma app_del_tail_head (u:uint) n : - n <= nb_digits u -> - app (del_tail n u) (del_head (nb_digits u - n) u) = u. -Proof. - unfold app, del_tail; rewrite rev_rev. - induction n. - - intros _; rewrite Nat.sub_0_r, del_head_nb_digits; simpl. - now rewrite revapp_rev_nil. - - intro Hn. - rewrite (del_head_nth (_ - _)); - [|now apply Nat.sub_lt; [|apply Nat.lt_0_succ]]. - rewrite Nat.sub_succ_r, <-Nat.sub_1_r. - rewrite <-(nth_revapp_l _ _ Nil Hn); fold (rev u). - rewrite <-revapp_revapp_1; [|now apply nb_digits_nth]. - rewrite <-(del_head_nth _ _); [|now rewrite nb_digits_rev]. - rewrite Nat.sub_1_r, Nat.succ_pred_pos; [|now apply Nat.lt_add_lt_sub_r]. - apply (IHn (le_Sn_le _ _ Hn)). +Lemma nb_digits_rev d : nb_digits (rev d) = nb_digits d. +Proof. now rewrite !nb_digits_spec, rev_spec, List.rev_length. Qed. + +Lemma nb_digits_del_head_sub d n : + n <= nb_digits d -> + nb_digits (del_head (nb_digits d - n) d) = n. +Proof. + rewrite !nb_digits_spec; intro Hn. + rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. + rewrite List.skipn_length, <-(Nat2Z.id (_ - _)). + rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. + rewrite (Nat2Z.inj_sub _ _ Hn). + rewrite Z.sub_sub_distr, Z.sub_diag; apply Nat2Z.id. +Qed. + +Lemma unorm_D0 u : unorm (D0 u) = unorm u. +Proof. reflexivity. Qed. + +Lemma app_nil_l d : app Nil d = d. +Proof. now simpl. Qed. + +Lemma app_nil_r d : app d Nil = d. +Proof. now apply to_list_inj; rewrite app_spec, List.app_nil_r. Qed. + +Lemma abs_app_int d d' : abs (app_int d d') = app (abs d) d'. +Proof. now case d. Qed. + +Lemma abs_norm d : abs (norm d) = unorm (abs d). +Proof. now case d as [u|u]; [|simpl; unfold unorm; case nzhead]. Qed. + +Lemma iter_D0_nzhead d : + Nat.iter (nb_digits d - nb_digits (nzhead d)) D0 (nzhead d) = d. +Proof. + induction d; [now simpl| |now rewrite Nat.sub_diag..]. + simpl nzhead; simpl nb_digits. + rewrite (Nat.sub_succ_l _ _ (nb_digits_nzhead _)). + now rewrite <-IHd at 4. +Qed. + +Lemma iter_D0_unorm d : + d <> Nil -> + Nat.iter (nb_digits d - nb_digits (unorm d)) D0 (unorm d) = d. +Proof. + case (uint_eq_dec (nzhead d) Nil); intro Hn. + { unfold unorm; rewrite Hn; simpl; intro H. + revert H Hn; induction d; [now simpl|intros _|now intros _..]. + case (uint_eq_dec d Nil); simpl; intros H Hn; [now rewrite H|]. + rewrite Nat.sub_0_r, (le_plus_minus 1 (nb_digits d)). + { now simpl; rewrite IHd. } + revert H; case d; [now simpl|intros u _; apply le_n_S, Nat.le_0_l..]. } + intros _; rewrite (unorm_nzhead _ Hn); apply iter_D0_nzhead. +Qed. + +Lemma nzhead_app_l d d' : + nb_digits d' < nb_digits (nzhead (app d d')) -> + nzhead (app d d') = app (nzhead d) d'. +Proof. + intro Hl; apply to_list_inj; revert Hl. + rewrite !nb_digits_spec, app_spec, !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]. + { now simpl; intro H; exfalso; revert H; apply le_not_lt, length_lnzhead. } + rewrite <-List.app_comm_cons. + now case h; [simpl; intro Hl; apply IHl|..]. +Qed. + +Lemma nzhead_app_r d d' : + nb_digits (nzhead (app d d')) <= nb_digits d' -> + nzhead (app d d') = nzhead d'. +Proof. + intro Hl; apply to_list_inj; revert Hl. + rewrite !nb_digits_spec, !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]; [now simpl|]. + rewrite <-List.app_comm_cons. + now case h; [| simpl; rewrite List.app_length; intro Hl; exfalso; revert Hl; + apply le_not_lt, le_plus_r..]. +Qed. + +Lemma nzhead_app_nil_r d d' : nzhead (app d d') = Nil -> nzhead d' = Nil. +Proof. +now intro H; generalize H; rewrite nzhead_app_r; [|rewrite H; apply Nat.le_0_l]. +Qed. + +Lemma nzhead_app_nil d d' : + nb_digits (nzhead (app d d')) <= nb_digits d' -> nzhead d = Nil. +Proof. + intro H; apply to_list_inj; revert H. + rewrite !nb_digits_spec, !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]; [now simpl|]. + now case h; [now simpl|..]; + simpl;intro H; exfalso; revert H; apply le_not_lt; + rewrite List.app_length; apply le_plus_r. +Qed. + +Lemma nzhead_app_nil_l d d' : nzhead (app d d') = Nil -> nzhead d = Nil. +Proof. + intro H; apply to_list_inj; generalize (f_equal to_list H); clear H. + rewrite !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]; [now simpl|]. + now rewrite <-List.app_comm_cons; case h. +Qed. + +Lemma unorm_app_zero d d' : + nb_digits (unorm (app d d')) <= nb_digits d' -> unorm d = zero. +Proof. + unfold unorm. + case (uint_eq_dec (nzhead (app d d')) Nil). + { now intro Hn; rewrite Hn, (nzhead_app_nil_l _ _ Hn). } + intro H; fold (unorm (app d d')); rewrite (unorm_nzhead _ H); intro H'. + case (uint_eq_dec (nzhead d) Nil); [now intros->|]. + intro H''; fold (unorm d); rewrite (unorm_nzhead _ H''). + exfalso; apply H''; revert H'; apply nzhead_app_nil. +Qed. + +Lemma app_int_nil_r d : app_int d Nil = d. +Proof. + now case d; intro d'; simpl; + rewrite <-(of_list_to_list (app _ _)), app_spec; + rewrite List.app_nil_r, of_list_to_list. +Qed. + +Lemma unorm_app_l d d' : + nb_digits d' < nb_digits (unorm (app d d')) -> + unorm (app d d') = app (unorm d) d'. +Proof. + case (uint_eq_dec d' Nil); [now intros->; rewrite !app_nil_r|intro Hd']. + case (uint_eq_dec (nzhead (app d d')) Nil). + { unfold unorm; intros->; simpl; intro H; exfalso; revert H; apply le_not_lt. + now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. } + intro Ha; rewrite (unorm_nzhead _ Ha). + intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn). + rewrite !nb_digits_spec, app_spec, List.app_length. + case (uint_eq_dec (nzhead d) Nil). + { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. } + now intro H; rewrite (unorm_nzhead _ H). +Qed. + +Lemma unorm_app_r d d' : + nb_digits (unorm (app d d')) <= nb_digits d' -> + unorm (app d d') = unorm d'. +Proof. + case (uint_eq_dec (nzhead (app d d')) Nil). + { now unfold unorm; intro H; rewrite H, (nzhead_app_nil_r _ _ H). } + intro Ha; rewrite (unorm_nzhead _ Ha). + case (uint_eq_dec (nzhead d') Nil). + { now intros H H'; exfalso; apply Ha; rewrite nzhead_app_r. } + intro Hd'; rewrite (unorm_nzhead _ Hd'); apply nzhead_app_r. +Qed. + +Lemma norm_app_int d d' : + nb_digits d' < nb_digits (unorm (app (abs d) d')) -> + norm (app_int d d') = app_int (norm d) d'. +Proof. + case (uint_eq_dec d' Nil); [now intros->; rewrite !app_int_nil_r|intro Hd']. + case d as [d|d]; [now simpl; intro H; apply f_equal, unorm_app_l|]. + simpl; unfold unorm. + case (uint_eq_dec (nzhead (app d d')) Nil). + { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt. + now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. } + set (m := match nzhead _ with Nil => _ | _ => _ end). + intro Ha. + replace m with (nzhead (app d d')). + 2:{ now unfold m; revert Ha; case nzhead. } + intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn). + case (uint_eq_dec (app (nzhead d) d') Nil). + { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt, Nat.le_0_l. } + clear m; set (m := match app _ _ with Nil => _ | _ => _ end). + intro Ha'. + replace m with (Neg (app (nzhead d) d')); [|now unfold m; revert Ha'; case app]. + case (uint_eq_dec (nzhead d) Nil). + { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. } + clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). + intro Hd. + now replace m with (Neg (nzhead d)); [|unfold m; revert Hd; case nzhead]. +Qed. + +Lemma del_head_nb_digits d : del_head (nb_digits d) d = Nil. +Proof. + apply to_list_inj. + rewrite nb_digits_spec, del_head_spec_small; [|now simpl]. + now rewrite List.skipn_all. +Qed. + +Lemma del_tail_nb_digits d : del_tail (nb_digits d) d = Nil. +Proof. now unfold del_tail; rewrite <-nb_digits_rev, del_head_nb_digits. Qed. + +Lemma del_head_app n d d' : + n <= nb_digits d -> del_head n (app d d') = app (del_head n d) d'. +Proof. + rewrite nb_digits_spec; intro Hn. + apply to_list_inj. + rewrite del_head_spec_small. + 2:{ now rewrite app_spec, List.app_length; apply le_plus_trans. } + rewrite !app_spec, (del_head_spec_small _ _ Hn). + rewrite List.skipn_app. + now rewrite (proj2 (Nat.sub_0_le _ _) Hn). +Qed. + +Lemma del_tail_app n d d' : + n <= nb_digits d' -> del_tail n (app d d') = app d (del_tail n d'). +Proof. + rewrite nb_digits_spec; intro Hn. + unfold del_tail. + rewrite <-(of_list_to_list (rev (app d d'))), rev_spec, app_spec. + rewrite List.rev_app_distr, <-!rev_spec, <-app_spec, of_list_to_list. + rewrite del_head_app; [|now rewrite nb_digits_spec, rev_spec, List.rev_length]. + apply to_list_inj. + rewrite rev_spec, !app_spec, !rev_spec. + now rewrite List.rev_app_distr, List.rev_involutive. +Qed. + +Lemma del_tail_app_int n d d' : + n <= nb_digits d' -> del_tail_int n (app_int d d') = app_int d (del_tail n d'). +Proof. now case d as [d|d]; simpl; intro H; rewrite del_tail_app. Qed. + +Lemma app_del_tail_head n (d:uint) : + n <= nb_digits d -> app (del_tail n d) (del_head (nb_digits d - n) d) = d. +Proof. + rewrite nb_digits_spec; intro Hn; unfold del_tail. + rewrite <-(of_list_to_list (app _ _)), app_spec, rev_spec. + rewrite del_head_spec_small; [|now rewrite rev_spec, List.rev_length]. + rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. + rewrite rev_spec. + set (n' := _ - n). + assert (Hn' : n = length (to_list d) - n'). + { now apply plus_minus; rewrite Nat.add_comm; symmetry; apply le_plus_minus_r. } + now rewrite Hn', <-List.firstn_skipn_rev, List.firstn_skipn, of_list_to_list. Qed. Lemma app_int_del_tail_head n (d:int) : - let ad := match d with Pos d | Neg d => d end in - n <= nb_digits ad -> - app_int (del_tail_int n d) (del_head (nb_digits ad - n) ad) = d. + n <= nb_digits (abs d) -> + app_int (del_tail_int n d) (del_head (nb_digits (abs d) - n) (abs d)) = d. Proof. now case d; clear d; simpl; intros u Hu; rewrite app_del_tail_head. Qed. +Lemma del_head_app_int_exact i f : + nb_digits f < nb_digits (unorm (app (abs i) f)) -> + del_head (nb_digits (unorm (app (abs i) f)) - nb_digits f) (unorm (app (abs i) f)) = f. +Proof. + simpl; intro Hnb; generalize Hnb; rewrite (unorm_app_l _ _ Hnb); clear Hnb. + replace (_ - _) with (nb_digits (unorm (abs i))). + - now rewrite del_head_app; [rewrite del_head_nb_digits|]. + - rewrite !nb_digits_spec, app_spec, List.app_length. + now rewrite Nat.add_comm, minus_plus. +Qed. + +Lemma del_tail_app_int_exact i f : + nb_digits f < nb_digits (unorm (app (abs i) f)) -> + del_tail_int (nb_digits f) (norm (app_int i f)) = norm i. +Proof. + simpl; intro Hnb. + rewrite (norm_app_int _ _ Hnb). + rewrite del_tail_app_int; [|now simpl]. + now rewrite del_tail_nb_digits, app_int_nil_r. +Qed. + (** Normalization on little-endian numbers *) Fixpoint nztail d := @@ -224,10 +474,13 @@ Proof. apply nzhead_revapp. Qed. +Lemma rev_rev d : rev (rev d) = d. +Proof. now apply to_list_inj; rewrite !rev_spec, List.rev_involutive. Qed. + Lemma rev_nztail_rev d : rev (nztail (rev d)) = nzhead d. Proof. - destruct (uint_dec (nztail (rev d)) Nil) as [H|H]. + destruct (uint_eq_dec (nztail (rev d)) Nil) as [H|H]. - rewrite H. unfold rev; simpl. rewrite <- (rev_rev d). symmetry. now apply nzhead_revapp_0. @@ -278,21 +531,9 @@ Proof. unfold unorm. now destruct nzhead. Qed. -Lemma unorm_D0 u : unorm (D0 u) = unorm u. -Proof. reflexivity. Qed. - Lemma unorm_iter_D0 n u : unorm (Nat.iter n D0 u) = unorm u. Proof. now induction n. Qed. -Lemma nb_digits_unorm u : - u <> Nil -> nb_digits (unorm u) <= nb_digits u. -Proof. - case u; clear u; [now simpl|intro u..]; [|now simpl..]. - intros _; unfold unorm. - case_eq (nzhead (D0 u)); [|now intros u' <-; apply nb_digits_nzhead..]. - intros _; apply le_n_S, Nat.le_0_l. -Qed. - Lemma del_head_nonnil n u : n < nb_digits u -> del_head n u <> Nil. Proof. @@ -311,73 +552,78 @@ Proof. now apply del_head_nonnil. Qed. -Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d. +Lemma nzhead_involutive d : nzhead (nzhead d) = nzhead d. Proof. now induction d. Qed. +#[deprecated(since="8.13",note="Use nzhead_involutive instead.")] +Notation nzhead_invol := nzhead_involutive (only parsing). -Lemma nztail_invol d : nztail (nztail d) = nztail d. +Lemma nztail_involutive d : nztail (nztail d) = nztail d. Proof. rewrite <-(rev_rev (nztail _)), <-(rev_rev (nztail d)), <-(rev_rev d). - now rewrite !rev_nztail_rev, nzhead_invol. + now rewrite !rev_nztail_rev, nzhead_involutive. Qed. +#[deprecated(since="8.13",note="Use nztail_involutive instead.")] +Notation nztail_invol := nztail_involutive (only parsing). -Lemma unorm_invol d : unorm (unorm d) = unorm d. +Lemma unorm_involutive d : unorm (unorm d) = unorm d. Proof. unfold unorm. destruct (nzhead d) eqn:E; trivial. destruct (nzhead_nonzero _ _ E). Qed. +#[deprecated(since="8.13",note="Use unorm_involutive instead.")] +Notation unorm_invol := unorm_involutive (only parsing). -Lemma norm_invol d : norm (norm d) = norm d. +Lemma norm_involutive d : norm (norm d) = norm d. Proof. unfold norm. destruct d. - - f_equal. apply unorm_invol. + - f_equal. apply unorm_involutive. - destruct (nzhead d) eqn:E; auto. destruct (nzhead_nonzero _ _ E). Qed. +#[deprecated(since="8.13",note="Use norm_involutive instead.")] +Notation norm_invol := norm_involutive (only parsing). + +Lemma lnzhead_neq_d0_head l l' : ~(lnzhead l = cons d0 l'). +Proof. now induction l as [|h t Il]; [|case h]. Qed. + +Lemma lnzhead_head_nd0 h t : h <> d0 -> lnzhead (cons h t) = cons h t. +Proof. now case h. Qed. Lemma nzhead_del_tail_nzhead_eq n u : nzhead u = u -> n < nb_digits u -> nzhead (del_tail n u) = del_tail n u. Proof. + rewrite nb_digits_spec, <-List.rev_length. intros Hu Hn. - assert (Hhd : forall u, - nzhead u = u <-> match nth 0 u with D0 _ => False | _ => True end). - { clear n u Hu Hn; intro u. - case u; clear u; [|intro u..]; [now simpl| |now simpl..]; simpl. - split; [|now simpl]. - apply nzhead_nonzero. } - assert (Hhd' : nth 0 (del_tail n u) = nth 0 u). - { rewrite <-(app_del_tail_head _ _ (le_Sn_le _ _ Hn)) at 2. - unfold app. - rewrite nth_revapp_l. - - rewrite <-(nth_revapp_l _ _ Nil). - + now fold (rev (rev (del_tail n u))); rewrite rev_rev. - + unfold del_tail; rewrite rev_rev. - rewrite nb_digits_del_head; rewrite nb_digits_rev. - * now rewrite <-Nat.lt_add_lt_sub_r. - * now apply Nat.lt_le_incl. - - unfold del_tail; rewrite rev_rev. - rewrite nb_digits_del_head; rewrite nb_digits_rev. - + now rewrite <-Nat.lt_add_lt_sub_r. - + now apply Nat.lt_le_incl. } - revert Hu; rewrite Hhd; intro Hu. - now rewrite Hhd, Hhd'. + apply to_list_inj; unfold del_tail. + rewrite nzhead_spec, rev_spec. + rewrite del_head_spec_small; [|now rewrite rev_spec; apply Nat.lt_le_incl]. + rewrite rev_spec. + rewrite List.skipn_rev, List.rev_involutive. + generalize (f_equal to_list Hu) Hn; rewrite nzhead_spec; intro Hu'. + case (to_list u) as [|h t]. + { simpl; intro H; exfalso; revert H; apply le_not_lt, Peano.le_0_n. } + intro Hn'; generalize (Nat.sub_gt _ _ Hn'); rewrite List.rev_length. + case (_ - _); [now simpl|]; intros n' _. + rewrite List.firstn_cons, lnzhead_head_nd0; [now simpl|]. + intro Hh; revert Hu'; rewrite Hh; apply lnzhead_neq_d0_head. Qed. Lemma nzhead_del_tail_nzhead n u : n < nb_digits (nzhead u) -> nzhead (del_tail n (nzhead u)) = del_tail n (nzhead u). -Proof. apply nzhead_del_tail_nzhead_eq, nzhead_invol. Qed. +Proof. apply nzhead_del_tail_nzhead_eq, nzhead_involutive. Qed. Lemma unorm_del_tail_unorm n u : n < nb_digits (unorm u) -> unorm (del_tail n (unorm u)) = del_tail n (unorm u). Proof. - case (uint_dec (nzhead u) Nil). + case (uint_eq_dec (nzhead u) Nil). - unfold unorm; intros->; case n; [now simpl|]; intro n'. now simpl; intro H; exfalso; generalize (lt_S_n _ _ H). - unfold unorm. @@ -396,7 +642,7 @@ Lemma norm_del_tail_int_norm n d : Proof. case d; clear d; intros u; simpl. - now intro H; simpl; rewrite unorm_del_tail_unorm. - - case (uint_dec (nzhead u) Nil); intro Hu. + - case (uint_eq_dec (nzhead u) Nil); intro Hu. + now rewrite Hu; case n; [|intros n' Hn'; generalize (lt_S_n _ _ Hn')]. + set (m := match nzhead u with Nil => Pos zero | _ => _ end). replace m with (Neg (nzhead u)); [|now unfold m; revert Hu; case nzhead]. @@ -418,7 +664,7 @@ Proof. generalize (nzhead_revapp d d'). generalize (nzhead_revapp_0 (nztail d) d'). generalize (nzhead_revapp (nztail d) d'). - rewrite nztail_invol. + rewrite nztail_involutive. now case nztail; [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl) |intros d'' H _ H' _; rewrite H; [rewrite H'|]..]. @@ -455,5 +701,10 @@ Proof. |rewrite H'; unfold r; clear m r H']; unfold norm; rewrite rev_rev, <-Hd''; - rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..]. + rewrite nzhead_revapp; rewrite nztail_involutive; [|rewrite Hd'']..]. +Qed. + +Lemma unorm_app_l_nil d d' : nzhead d = Nil -> unorm (app d d') = unorm d'. +Proof. + now unfold unorm; rewrite <-nzhead_app_nzhead; intros->; rewrite app_nil_l. Qed. diff --git a/theories/Numbers/DecimalN.v b/theories/Numbers/DecimalN.v index 8bc5c38fb5..a5dd97f24b 100644 --- a/theories/Numbers/DecimalN.v +++ b/theories/Numbers/DecimalN.v @@ -74,7 +74,7 @@ Proof. destruct (norm d) eqn:Hd; intros [= <-]. unfold N.to_int. rewrite Unsigned.to_of. f_equal. revert Hd; destruct d; simpl. - - intros [= <-]. apply unorm_invol. + - intros [= <-]. apply unorm_involutive. - destruct (nzhead d); now intros [= <-]. Qed. @@ -93,7 +93,7 @@ Qed. Lemma of_int_norm d : N.of_int (norm d) = N.of_int d. Proof. - unfold N.of_int. now rewrite norm_invol. + unfold N.of_int. now rewrite norm_involutive. Qed. Lemma of_inj_pos d d' : diff --git a/theories/Numbers/DecimalNat.v b/theories/Numbers/DecimalNat.v index 1962ac5d9d..4fee40caa2 100644 --- a/theories/Numbers/DecimalNat.v +++ b/theories/Numbers/DecimalNat.v @@ -270,7 +270,7 @@ Proof. destruct (norm d) eqn:Hd; intros [= <-]. unfold Nat.to_int. rewrite Unsigned.to_of. f_equal. revert Hd; destruct d; simpl. - - intros [= <-]. apply unorm_invol. + - intros [= <-]. apply unorm_involutive. - destruct (nzhead d); now intros [= <-]. Qed. @@ -289,7 +289,7 @@ Qed. Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d. Proof. - unfold Nat.of_int. now rewrite norm_invol. + unfold Nat.of_int. now rewrite norm_involutive. Qed. Lemma of_inj_pos d d' : diff --git a/theories/Numbers/DecimalQ.v b/theories/Numbers/DecimalQ.v index c51cced024..2027813eec 100644 --- a/theories/Numbers/DecimalQ.v +++ b/theories/Numbers/DecimalQ.v @@ -15,455 +15,413 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith. -Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q. +Lemma of_IQmake_to_decimal num den : + match IQmake_to_decimal num den with + | None => True + | Some (DecimalExp _ _ _) => False + | Some (Decimal i f) => of_decimal (Decimal i f) = IQmake (IZ_of_Z num) den + end. Proof. - cut (match to_decimal q with None => True | Some d => of_decimal d = q end). - { now case to_decimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. } - destruct q as (num, den). - unfold to_decimal; simpl. - generalize (DecimalPos.Unsigned.nztail_to_uint den). - case Decimal.nztail; intros u n. - case u; clear u; [intros; exact I|intros; exact I|intro u|intros; exact I..]. - case u; clear u; [|intros; exact I..]. - unfold Pos.of_uint, Pos.of_uint_acc; rewrite N.mul_1_l. - case n. - - unfold of_decimal, app_int, app, Z.to_int; simpl. - intro H; inversion H as (H1); clear H H1. - case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_uint pnum)))..]. - + rewrite rev_rev; simpl. - now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. - + rewrite rev_rev; simpl. - now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. - - clear n; intros n H. - injection H; clear H; intros ->. - case Nat.ltb. - + unfold of_decimal. - rewrite of_to. - apply f_equal2; [|now simpl]. - unfold app_int, app, Z.to_int; simpl. - now case num; - [|intro pnum; fold (rev (rev (Pos.to_uint pnum))); - rewrite rev_rev; unfold Z.of_int, Z.of_uint; - rewrite DecimalPos.Unsigned.of_to..]. - + unfold of_decimal; case Nat.ltb_spec; intro Hn; simpl. - * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply le_Sn_le]. - rewrite Z.sub_sub_distr, Z.sub_diag; simpl. - rewrite <-(of_to num) at 4. - now revert Hn; case Z.to_int; clear num; intros pnum Hn; simpl; - (rewrite app_del_tail_head; [|now apply le_Sn_le]). - * revert Hn. - set (anum := match Z.to_int num with Pos i => i | _ => _ end). - intro Hn. - assert (H : exists l, nb_digits anum = S l). - { exists (Nat.pred (nb_digits anum)); apply S_pred_pos. - now unfold anum; case num; - [apply Nat.lt_0_1| - intro pnum; apply nb_digits_pos, Unsigned.to_uint_nonnil..]. } - destruct H as (l, Hl); rewrite Hl. - assert (H : forall n d, (nb_digits (Nat.iter n D0 d) = n + nb_digits d)%nat). - { now intros n'; induction n'; intro d; [|simpl; rewrite IHn']. } - rewrite H, Hl. - rewrite Nat.add_succ_r, Nat.sub_add; [|now apply le_S_n; rewrite <-Hl]. - assert (H' : forall n d, Pos.of_uint (Nat.iter n D0 d) = Pos.of_uint d). - { now intro n'; induction n'; intro d; [|simpl; rewrite IHn']. } - now unfold anum; case num; simpl; [|intro pnum..]; - unfold app, Z.of_uint; simpl; - rewrite H', ?DecimalPos.Unsigned.of_to. + unfold IQmake_to_decimal. + generalize (Unsigned.nztail_to_uint den). + case Decimal.nztail; intros den' e_den'. + case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'. + case den'; [ |now simpl..]; clear den'. + case e_den' as [|e_den']; simpl; intro H; injection H; clear H; intros->. + { now unfold of_decimal; simpl; rewrite app_int_nil_r, DecimalZ.of_to. } + replace (10 ^ _)%positive with (Nat.iter (S e_den') (Pos.mul 10) 1%positive). + 2:{ induction e_den' as [|n IHn]; [now simpl| ]. + now rewrite SuccNat2Pos.inj_succ, Pos.pow_succ_r, <-IHn. } + case Nat.ltb_spec; intro He_den'. + - unfold of_decimal; simpl. + rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl]. + rewrite DecimalZ.of_to. + now rewrite nb_digits_del_head_sub; [|now apply Nat.lt_le_incl]. + - unfold of_decimal; simpl. + rewrite nb_digits_iter_D0. + apply f_equal2. + + apply f_equal, DecimalZ.to_int_inj. + rewrite DecimalZ.to_of. + rewrite <-(DecimalZ.of_to num), DecimalZ.to_of. + case (Z.to_int num); clear He_den' num; intro num; simpl. + * unfold app; simpl. + now rewrite unorm_D0, unorm_iter_D0, unorm_involutive. + * case (uint_eq_dec (nzhead num) Nil); [|intro Hn]. + { intros->; simpl; unfold app; simpl. + now rewrite unorm_D0, unorm_iter_D0. } + replace (match nzhead num with Nil => _ | _ => _ end) + with (Neg (nzhead num)); [|now revert Hn; case nzhead]. + simpl. + rewrite nzhead_iter_D0, nzhead_involutive. + now revert Hn; case nzhead. + + revert He_den'; case nb_digits as [|n]; [now simpl; rewrite Nat.add_0_r|]. + intro Hn. + rewrite Nat.add_succ_r, Nat.add_comm. + now rewrite <-le_plus_minus; [|apply le_S_n]. Qed. -(* normalize without fractional part, for instance norme 12.3e-1 is 123e-2 *) -Definition dnorme (d:decimal) : decimal := - let '(i, f, e) := - match d with - | Decimal i f => (i, f, Pos Nil) - | DecimalExp i f e => (i, f, e) - end in - let i := norm (app_int i f) in - let e := norm (Z.to_int (Z.of_int e - Z.of_nat (nb_digits f))) in - match e with - | Pos zero => Decimal i Nil - | _ => DecimalExp i Nil e +Lemma IZ_of_Z_IZ_to_Z z z' : IZ_to_Z z = Some z' -> IZ_of_Z z' = z. +Proof. now case z as [| |p|p]; [|intro H; injection H; intros<-..]. Qed. + +Lemma of_IQmake_to_decimal' num den : + match IQmake_to_decimal' num den with + | None => True + | Some (DecimalExp _ _ _) => False + | Some (Decimal i f) => of_decimal (Decimal i f) = IQmake num den end. +Proof. + unfold IQmake_to_decimal'. + case_eq (IZ_to_Z num); [intros num' Hnum'|now simpl]. + generalize (of_IQmake_to_decimal num' den). + case IQmake_to_decimal as [d|]; [|now simpl]. + case d as [i f|]; [|now simpl]. + now rewrite (IZ_of_Z_IZ_to_Z _ _ Hnum'). +Qed. + +Lemma of_to (q:IQ) : forall d, to_decimal q = Some d -> of_decimal d = q. +Proof. + intro d. + case q as [num den|q q'|q q']; simpl. + - generalize (of_IQmake_to_decimal' num den). + case IQmake_to_decimal' as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + now intros H H'; injection H'; clear H'; intros <-. + - case q as [num den| |]; [|now simpl..]. + case q' as [num' den'| |]; [|now simpl..]. + case num' as [z p| | |]; [|now simpl..]. + case (Z.eq_dec z 10); [intros->|]. + 2:{ case z; [now simpl| |now simpl]; intro pz'. + case pz'; [intros d0..| ]; [now simpl| |now simpl]. + case d0; [intros d1..| ]; [ |now simpl..]. + case d1; [intros d2..| ]; [now simpl| |now simpl]. + now case d2. } + case (Pos.eq_dec den' 1%positive); [intros->|now case den']. + generalize (of_IQmake_to_decimal' num den). + case IQmake_to_decimal' as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros <-; clear num den. + intros H; injection H; clear H; intros<-. + unfold of_decimal; simpl. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + - case q as [num den| |]; [|now simpl..]. + case q' as [num' den'| |]; [|now simpl..]. + case num' as [z p| | |]; [|now simpl..]. + case (Z.eq_dec z 10); [intros->|]. + 2:{ case z; [now simpl| |now simpl]; intro pz'. + case pz'; [intros d0..| ]; [now simpl| |now simpl]. + case d0; [intros d1..| ]; [ |now simpl..]. + case d1; [intros d2..| ]; [now simpl| |now simpl]. + now case d2. } + case (Pos.eq_dec den' 1%positive); [intros->|now case den']. + generalize (of_IQmake_to_decimal' num den). + case IQmake_to_decimal' as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros <-; clear num den. + intros H; injection H; clear H; intros<-. + unfold of_decimal; simpl. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. +Qed. -(* normalize without exponent part, for instance norme 12.3e-1 is 1.23 *) -Definition dnormf (d:decimal) : decimal := - match dnorme d with - | Decimal i _ => Decimal i Nil - | DecimalExp i _ e => - match Z.of_int e with - | Z0 => Decimal i Nil - | Zpos e => Decimal (norm (app_int i (Pos.iter D0 Nil e))) Nil - | Zneg e => - let ne := Pos.to_nat e in - let ai := match i with Pos d | Neg d => d end in - let ni := nb_digits ai in - if ne <? ni then - Decimal (del_tail_int ne i) (del_head (ni - ne) ai) - else - let z := match i with Pos _ => Pos zero | Neg _ => Neg zero end in - Decimal z (Nat.iter (ne - ni) D0 ai) +Definition dnorm (d:decimal) : decimal := + let norm_i i f := + match i with + | Pos i => Pos (unorm i) + | Neg i => match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end + end in + match d with + | Decimal i f => Decimal (norm_i i f) f + | DecimalExp i f e => + match norm e with + | Pos zero => Decimal (norm_i i f) f + | e => DecimalExp (norm_i i f) f e end end. -Lemma dnorme_spec d : - match dnorme d with - | Decimal i Nil => i = norm i - | DecimalExp i Nil e => i = norm i /\ e = norm e /\ e <> Pos zero - | _ => False +Lemma dnorm_spec_i d : + let (i, f) := + match d with Decimal i f => (i, f) | DecimalExp i f _ => (i, f) end in + let i' := match dnorm d with Decimal i _ => i | DecimalExp i _ _ => i end in + match i with + | Pos i => i' = Pos (unorm i) + | Neg i => + (i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil)) + \/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil)) end. Proof. - case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl. - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. - + now rewrite norm_invol. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - replace m with r; [now unfold r; rewrite !norm_invol|]. - unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. - + now rewrite norm_invol. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - replace m with r; [now unfold r; rewrite !norm_invol|]. - unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. + case d as [i f|i f e]; case i as [i|i]. + - now simpl. + - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha. + + rewrite Ha; right; split; [now simpl|split]. + * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha). + * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha). + + left; split; [now revert Ha; case nzhead|]. + case (uint_eq_dec (nzhead i) Nil). + * intro Hi; right; intro Hf; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + * now intro H; left. + - simpl; case (norm e); clear e; intro e; [|now simpl]. + now case e; clear e; [|intro e..]; [|case e|..]. + - simpl. + set (m := match nzhead _ with Nil => _ | _ => _ end). + set (m' := match _ with Decimal _ _ => _ | _ => _ end). + replace m' with m. + 2:{ unfold m'; case (norm e); clear m' e; intro e; [|now simpl]. + now case e; clear e; [|intro e..]; [|case e|..]. } + unfold m; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha. + + rewrite Ha; right; split; [now simpl|split]. + * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha). + * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha). + + left; split; [now revert Ha; case nzhead|]. + case (uint_eq_dec (nzhead i) Nil). + * intro Hi; right; intro Hf; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + * now intro H; left. +Qed. + +Lemma dnorm_spec_f d : + let f := match d with Decimal _ f => f | DecimalExp _ f _ => f end in + let f' := match dnorm d with Decimal _ f => f | DecimalExp _ f _ => f end in + f' = f. +Proof. + case d as [i f|i f e]; [now simpl|]. + simpl; case (int_eq_dec (norm e) (Pos zero)); [now intros->|intro He]. + set (i' := match i with Pos _ => _ | _ => _ end). + set (m := match norm e with Pos Nil => _ | _ => _ end). + replace m with (DecimalExp i' f (norm e)); [now simpl|]. + unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. Qed. -Lemma dnormf_spec d : - match dnormf d with - | Decimal i f => i = Neg zero \/ i = norm i - | _ => False +Lemma dnorm_spec_e d : + match d, dnorm d with + | Decimal _ _, Decimal _ _ => True + | DecimalExp _ _ e, Decimal _ _ => norm e = Pos zero + | DecimalExp _ _ e, DecimalExp _ _ e' => e' = norm e /\ e' <> Pos zero + | Decimal _ _, DecimalExp _ _ _ => False end. Proof. - case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl. - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. - + now right; rewrite norm_invol. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. } - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe'; - [now right; rewrite norm_invol..|]. - case Nat.ltb_spec. - * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right. - * now intros _; case norm; intros _; [right|left]. - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. - + now right; rewrite norm_invol. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. } - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe'; - [now right; rewrite norm_invol..|]. - case Nat.ltb_spec. - * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right. - * now intros _; case norm; intros _; [right|left]. + case d as [i f|i f e]; [now simpl|]. + simpl; case (int_eq_dec (norm e) (Pos zero)); [now intros->|intro He]. + set (i' := match i with Pos _ => _ | _ => _ end). + set (m := match norm e with Pos Nil => _ | _ => _ end). + replace m with (DecimalExp i' f (norm e)); [now simpl|]. + unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. Qed. -Lemma dnorme_invol d : dnorme (dnorme d) = dnorme d. +Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm d. Proof. - case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl. - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); intro Hne'. - + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. - revert Hne'. - rewrite <-to_of. - change (Pos zero) with (Z.to_int 0). - intro H; generalize (to_int_inj _ _ H); clear H. - unfold e'; rewrite DecimalZ.of_to. - now case f; [rewrite app_int_nil_r|..]. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. } - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol. - rewrite app_int_nil_r, norm_invol. - set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); intro Hne'. - + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. - revert Hne'. - rewrite <-to_of. - change (Pos zero) with (Z.to_int 0). - intro H; generalize (to_int_inj _ _ H); clear H. - unfold e'; rewrite DecimalZ.of_to. - now case f; [rewrite app_int_nil_r|..]. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. } - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol. - rewrite app_int_nil_r, norm_invol. - set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. + case d as [i f|i f e]; case i as [i|i]. + - now simpl; rewrite unorm_involutive. + - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. + set (m := match nzhead _ with Nil =>_ | _ => _ end). + replace m with (Neg (unorm i)). + 2:{ now unfold m; revert Ha; case nzhead. } + case (uint_eq_dec (nzhead i) Nil); intro Hi. + + unfold unorm; rewrite Hi; simpl. + case (uint_eq_dec (nzhead f) Nil). + * intro Hf; exfalso; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + * now case nzhead. + + rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. + now revert Ha; case nzhead. + - simpl; case (int_eq_dec (norm e) (Pos zero)); intro He. + + now rewrite He; simpl; rewrite unorm_involutive. + + set (m := match norm e with Pos Nil => _ | _ => _ end). + replace m with (DecimalExp (Pos (unorm i)) f (norm e)). + 2:{ unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. } + simpl; rewrite norm_involutive, unorm_involutive. + revert He; case (norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. + - simpl; case (int_eq_dec (norm e) (Pos zero)); intro He. + + rewrite He; simpl. + case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. + set (m := match nzhead _ with Nil =>_ | _ => _ end). + replace m with (Neg (unorm i)). + 2:{ now unfold m; revert Ha; case nzhead. } + case (uint_eq_dec (nzhead i) Nil); intro Hi. + * unfold unorm; rewrite Hi; simpl. + case (uint_eq_dec (nzhead f) Nil). + -- intro Hf; exfalso; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + -- now case nzhead. + * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. + now revert Ha; case nzhead. + + set (m := match norm e with Pos Nil => _ | _ => _ end). + pose (i' := match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end). + replace m with (DecimalExp i' f (norm e)). + 2:{ unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. } + simpl; rewrite norm_involutive. + set (i'' := match i' with Pos _ => _ | _ => _ end). + clear m; set (m := match norm e with Pos Nil => _ | _ => _ end). + replace m with (DecimalExp i'' f (norm e)). + 2:{ unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. } + unfold i'', i'. + case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. + fold i'; replace i' with (Neg (unorm i)). + 2:{ now unfold i'; revert Ha; case nzhead. } + case (uint_eq_dec (nzhead i) Nil); intro Hi. + * unfold unorm; rewrite Hi; simpl. + case (uint_eq_dec (nzhead f) Nil). + -- intro Hf; exfalso; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + -- now case nzhead. + * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. + now revert Ha; case nzhead. Qed. -Lemma dnormf_invol d : dnormf (dnormf d) = dnormf d. +Lemma IZ_to_Z_IZ_of_Z z : IZ_to_Z (IZ_of_Z z) = Some z. +Proof. now case z. Qed. + +Lemma dnorm_i_exact i f : + (nb_digits f < nb_digits (unorm (app (abs i) f)))%nat -> + match i with + | Pos i => Pos (unorm i) + | Neg i => + match nzhead (app i f) with + | Nil => Pos zero + | _ => Neg (unorm i) + end + end = norm i. Proof. - case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl. - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); intro Hne'. - + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. - revert Hne'. - rewrite <-to_of. - change (Pos zero) with (Z.to_int 0). - intro H; generalize (to_int_inj _ _ H); clear H. - unfold e'; rewrite DecimalZ.of_to. - now case f; [rewrite app_int_nil_r|..]. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. } - rewrite of_int_norm. - case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe'; - [now simpl; rewrite app_int_nil_r, norm_invol..|]. - case Nat.ltb_spec; intro Hpe'. - * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl]. - simpl. - rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l. - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - rewrite positive_nat_Z; simpl. - unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl]. - now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe'). - * simpl. - rewrite nb_digits_iter_D0. - rewrite (Nat.sub_add _ _ Hpe'). - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - rewrite positive_nat_Z; simpl. - unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - revert Hpe'. - set (i' := norm (app_int i f)). - case_eq i'; intros u Hu Hpe'. - ++ simpl; unfold app; simpl. - rewrite unorm_D0, unorm_iter_D0. - assert (Hu' : unorm u = u). - { generalize (f_equal norm Hu). - unfold i'; rewrite norm_invol; fold i'. - now simpl; rewrite Hu; intro H; injection H. } - now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe'). - ++ simpl; rewrite nzhead_iter_D0. - assert (Hu' : nzhead u = u). - { generalize (f_equal norm Hu). - unfold i'; rewrite norm_invol; fold i'. - now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. } - rewrite Hu'. - assert (Hu'' : u <> Nil). - { intro H; revert Hu; rewrite H; unfold i'. - now case app_int; intro u'; [|simpl; case nzhead]. } - set (m := match u with Nil => Pos zero | _ => _ end). - assert (H : m = Neg u); [|rewrite H; clear m H]. - { now revert Hu''; unfold m; case u. } - now rewrite (proj2 (Nat.ltb_ge _ _) Hpe'). - - set (e' := Z.to_int _). - case (int_eq_dec (norm e') (Pos zero)); intro Hne'. - + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. - revert Hne'. - rewrite <-to_of. - change (Pos zero) with (Z.to_int 0). - intro H; generalize (to_int_inj _ _ H); clear H. - unfold e'; rewrite DecimalZ.of_to. - now case f; [rewrite app_int_nil_r|..]. - + set (r := DecimalExp _ _ _). - set (m := match norm e' with Pos zero => _ | _ => _ end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. - now case e''; [|intro e'''; case e'''..]. } - rewrite of_int_norm. - case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe'; - [now simpl; rewrite app_int_nil_r, norm_invol..|]. - case Nat.ltb_spec; intro Hpe'. - * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl]. - simpl. - rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l. - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - rewrite positive_nat_Z; simpl. - unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl]. - now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe'). - * simpl. - rewrite nb_digits_iter_D0. - rewrite (Nat.sub_add _ _ Hpe'). - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - rewrite positive_nat_Z; simpl. - unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - revert Hpe'. - set (i' := norm (app_int i f)). - case_eq i'; intros u Hu Hpe'. - ++ simpl; unfold app; simpl. - rewrite unorm_D0, unorm_iter_D0. - assert (Hu' : unorm u = u). - { generalize (f_equal norm Hu). - unfold i'; rewrite norm_invol; fold i'. - now simpl; rewrite Hu; intro H; injection H. } - now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe'). - ++ simpl; rewrite nzhead_iter_D0. - assert (Hu' : nzhead u = u). - { generalize (f_equal norm Hu). - unfold i'; rewrite norm_invol; fold i'. - now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. } - rewrite Hu'. - assert (Hu'' : u <> Nil). - { intro H; revert Hu; rewrite H; unfold i'. - now case app_int; intro u'; [|simpl; case nzhead]. } - set (m := match u with Nil => Pos zero | _ => _ end). - assert (H : m = Neg u); [|rewrite H; clear m H]. - { now revert Hu''; unfold m; case u. } - now rewrite (proj2 (Nat.ltb_ge _ _) Hpe'). + case i as [ni|ni]; [now simpl|]; simpl. + case (uint_eq_dec (nzhead (app ni f)) Nil); intro Ha. + { now rewrite Ha, (nzhead_app_nil_l _ _ Ha). } + rewrite (unorm_nzhead _ Ha). + set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (Neg (unorm ni)); [|now unfold m; revert Ha; case nzhead]. + case (uint_eq_dec (nzhead ni) Nil); intro Hni. + { rewrite <-nzhead_app_nzhead, Hni, app_nil_l. + intro H; exfalso; revert H; apply le_not_lt, nb_digits_nzhead. } + clear m; set (m := match nzhead ni with Nil => _ | _ => _ end). + replace m with (Neg (nzhead ni)); [|now unfold m; revert Hni; case nzhead]. + now rewrite (unorm_nzhead _ Hni). +Qed. + +Lemma dnorm_i_exact' i f : + (nb_digits (unorm (app (abs i) f)) <= nb_digits f)%nat -> + match i with + | Pos i => Pos (unorm i) + | Neg i => + match nzhead (app i f) with + | Nil => Pos zero + | _ => Neg (unorm i) + end + end = + match norm (app_int i f) with + | Pos _ => Pos zero + | Neg _ => Neg zero + end. +Proof. + case i as [ni|ni]; simpl. + { now intro Hnb; rewrite (unorm_app_zero _ _ Hnb). } + unfold unorm. + case (uint_eq_dec (nzhead (app ni f)) Nil); intro Hn. + { now rewrite Hn. } + set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (nzhead (app ni f)). + 2:{ now unfold m; revert Hn; case nzhead. } + clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (Neg (unorm ni)). + 2:{ now unfold m, unorm; revert Hn; case nzhead. } + clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (Neg (nzhead (app ni f))). + 2:{ now unfold m; revert Hn; case nzhead. } + rewrite <-(unorm_nzhead _ Hn). + now intro H; rewrite (unorm_app_zero _ _ H). Qed. -Lemma to_of (d:decimal) : - to_decimal (of_decimal d) = Some (dnorme d) - \/ to_decimal (of_decimal d) = Some (dnormf d). +Lemma to_of (d:decimal) : to_decimal (of_decimal d) = Some (dnorm d). Proof. - unfold to_decimal. - pose (t10 := fun y => ((y + y~0~0)~0)%positive). - assert (H : exists e_den, - Decimal.nztail (Pos.to_uint (Qden (of_decimal d))) = (D1 Nil, e_den)). - { assert (H : forall p, - Decimal.nztail (Pos.to_uint (Pos.iter t10 1%positive p)) - = (D1 Nil, Pos.to_nat p)). - { intro p; rewrite Pos2Nat.inj_iter. - fold (Nat.iter (Pos.to_nat p) t10 1%positive). - induction (Pos.to_nat p); [now simpl|]. - rewrite DecimalPos.Unsigned.nat_iter_S. - unfold Pos.to_uint. - change (Pos.to_little_uint _) - with (Unsigned.to_lu (10 * N.pos (Nat.iter n t10 1%positive))). - rewrite Unsigned.to_ldec_tenfold. - revert IHn; unfold Pos.to_uint. - unfold Decimal.nztail; rewrite !rev_rev; simpl. - set (f'' := _ (Pos.to_little_uint _)). - now case f''; intros r n' H; inversion H. } - case d; intros i f; [|intro e]; unfold of_decimal; simpl. - - case (- Z.of_nat _)%Z; [|intro p..]; simpl; [now exists O..|]. - exists (Pos.to_nat p); apply H. - - case (_ - _)%Z; [|intros p..]; simpl; [now exists O..|]. - exists (Pos.to_nat p); apply H. } - generalize (DecimalPos.Unsigned.nztail_to_uint (Qden (of_decimal d))). - destruct H as (e, He); rewrite He; clear He; simpl. - assert (Hn1 : forall p, N.pos (Pos.iter t10 1%positive p) = 1%N -> False). - { intro p. - rewrite Pos2Nat.inj_iter. - case_eq (Pos.to_nat p); [|now simpl]. - intro H; exfalso; apply (lt_irrefl O). - rewrite <-H at 2; apply Pos2Nat.is_pos. } - assert (Ht10inj : forall n m, t10 n = t10 m -> n = m). - { intros n m H; generalize (f_equal Z.pos H); clear H. - change (Z.pos (t10 n)) with (Z.mul 10 (Z.pos n)). - change (Z.pos (t10 m)) with (Z.mul 10 (Z.pos m)). - rewrite Z.mul_comm, (Z.mul_comm 10). - intro H; generalize (f_equal (fun z => Z.div z 10) H); clear H. - now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. } - assert (Hinj : forall n m, - Nat.iter n t10 1%positive = Nat.iter m t10 1%positive -> n = m). - { induction n; [now intro m; case m|]. - intro m; case m; [now simpl|]; clear m; intro m. - rewrite !Unsigned.nat_iter_S. - intro H; generalize (Ht10inj _ _ H); clear H; intro H. - now rewrite (IHn _ H). } - case e; clear e; [|intro e]; simpl; unfold of_decimal, dnormf, dnorme. - - case d; clear d; intros i f; [|intro e]; simpl. - + intro H; left; revert H. - generalize (nb_digits_pos f). - case f; - [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2; - case nb_digits; simpl; - [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..]. - now intros _ _; simpl; rewrite to_of. - + intro H; right; revert H. - rewrite <-to_of, DecimalZ.of_to. - set (emf := (_ - _)%Z). - case_eq emf; [|intro pemf..]. - * now simpl; rewrite to_of. - * set (r := DecimalExp _ _ _). - set (m := match _ with Pos _ => _ | _ => r end). - assert (H : m = r). - { unfold m, Z.to_int. - generalize (Unsigned.to_uint_nonzero pemf). - now case Pos.to_uint; [|intro u; case u..]. } - rewrite H; unfold r; clear H m r. - rewrite DecimalZ.of_to. - simpl Qnum. - intros Hpemf _. - apply f_equal; apply f_equal2; [|reflexivity]. - rewrite !Pos2Nat.inj_iter. - set (n := _ pemf). - fold (Nat.iter n (Z.mul 10) (Z.of_int (app_int i f))). - fold (Nat.iter n D0 Nil). - rewrite <-of_int_iter_D0, to_of. - now rewrite norm_app_int_norm; [|induction n]. - * simpl Qden; intros _ H; exfalso; revert H; apply Hn1. - - case d; clear d; intros i f; [|intro e']; simpl. - + case_eq (nb_digits f); [|intros nf' Hnf']; - [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1|]. - unfold Z.of_nat, Z.opp. - simpl Qden. - intro H; injection H; clear H; unfold Pos.pow. - rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (SuccNat2Pos.inj _ _ ((Pos2Nat.inj _ _ H))); clear H. - intro He; rewrite <-He; clear e He. - simpl Qnum. - case Nat.ltb; [left|right]. - * now rewrite <-to_of, DecimalZ.of_to, to_of. - * rewrite to_of. - set (nif := norm _). - set (anif := match nif with Pos i0 => i0 | _ => _ end). - set (r := DecimalExp nif Nil _). - set (m := match _ with Pos _ => _ | _ => r end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { now unfold m; rewrite <-to_of, DecimalZ.of_to. } - rewrite <-to_of, !DecimalZ.of_to. - fold anif. - now rewrite SuccNat2Pos.id_succ. - + set (nemf := (_ - _)%Z); intro H. - assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H]. - { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf]; - simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1. } - destruct H' as (pnemf,Hpnemf); rewrite Hpnemf. - simpl Qden. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H. - intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf. - simpl Qnum. - case Nat.ltb; [left|right]. - * now rewrite <-to_of, DecimalZ.of_to, to_of. - * rewrite to_of. - set (nif := norm _). - set (anif := match nif with Pos i0 => i0 | _ => _ end). - set (r := DecimalExp nif Nil _). - set (m := match _ with Pos _ => _ | _ => r end). - assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. - { now unfold m; rewrite <-to_of, DecimalZ.of_to. } - rewrite <-to_of, !DecimalZ.of_to. - fold anif. - now rewrite SuccNat2Pos.id_succ. + case d as [i f|i f e]. + - unfold of_decimal; simpl; unfold IQmake_to_decimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_decimal; simpl. + change (fun _ : positive => _) with (Pos.mul 10). + rewrite nztail_to_uint_pow10, to_of. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + + rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + + rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + * rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + * rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. + - unfold of_decimal; simpl. + rewrite <-to_of. + case (Z.of_int e); clear e; [|intro e..]; simpl. + + unfold IQmake_to_decimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_decimal; simpl. + change (fun _ : positive => _) with (Pos.mul 10). + rewrite nztail_to_uint_pow10, to_of. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + * rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + -- rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + -- rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. + + unfold IQmake_to_decimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_decimal; simpl. + change (fun _ : positive => _) with (Pos.mul 10). + rewrite nztail_to_uint_pow10, to_of. + generalize (Unsigned.to_uint_nonzero e); intro He. + set (dnorm_i := match i with Pos _ => _ | _ => _ end). + set (m := match Pos.to_uint e with Nil => _ | _ => _ end). + replace m with (DecimalExp dnorm_i f (Pos (Pos.to_uint e))). + 2:{ now unfold m; revert He; case (Pos.to_uint e); [|intro u; case u|..]. } + clear m; unfold dnorm_i. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + * rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + -- rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + -- rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. + + unfold IQmake_to_decimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_decimal; simpl. + change (fun _ : positive => _) with (Pos.mul 10). + rewrite nztail_to_uint_pow10, to_of. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + * rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + -- rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + -- rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. Qed. (** Some consequences *) @@ -478,84 +436,24 @@ Proof. now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). Qed. -Lemma to_decimal_surj d : - exists q, to_decimal q = Some (dnorme d) \/ to_decimal q = Some (dnormf d). +Lemma to_decimal_surj d : exists q, to_decimal q = Some (dnorm d). Proof. exists (of_decimal d). apply to_of. Qed. -Lemma of_decimal_dnorme d : of_decimal (dnorme d) = of_decimal d. +Lemma of_decimal_dnorm d : of_decimal (dnorm d) = of_decimal d. +Proof. now apply to_decimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed. + +Lemma of_inj d d' : of_decimal d = of_decimal d' -> dnorm d = dnorm d'. Proof. - unfold of_decimal, dnorme. - destruct d. - - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - case_eq (nb_digits f); [|intro nf]; intro Hnf. - + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to. - + simpl; rewrite Z.sub_0_r. - unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - rewrite app_int_nil_r. - now rewrite <-DecimalZ.to_of, DecimalZ.of_to. - - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - set (emf := (_ - _)%Z). - case_eq emf; [|intro pemf..]; intro Hemf. - + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to. - + simpl. - set (r := DecimalExp _ Nil _). - set (m := match Pos.to_uint pemf with zero => _ | _ => r end). - assert (H : m = r); [|rewrite H; unfold r; clear m r H]. - { generalize (Unsigned.to_uint_nonzero pemf). - now unfold m; case Pos.to_uint; [|intro u; case u|..]. } - simpl; rewrite Z.sub_0_r. - unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - rewrite app_int_nil_r. - now rewrite <-DecimalZ.to_of, DecimalZ.of_to. - + simpl. - unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - rewrite app_int_nil_r. - now rewrite <-DecimalZ.to_of, DecimalZ.of_to. + intro H. + apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end) + (Some (dnorm d)) (Some (dnorm d'))). + now rewrite <- !to_of, H. Qed. -Lemma of_decimal_dnormf d : of_decimal (dnormf d) = of_decimal d. +Lemma of_iff d d' : of_decimal d = of_decimal d' <-> dnorm d = dnorm d'. Proof. - rewrite <-(of_decimal_dnorme d). - unfold of_decimal, dnormf. - assert (H : match dnorme d with Decimal _ f | DecimalExp _ f _ => f end = Nil). - { now unfold dnorme; destruct d; - (case norm; intro d; [case d; [|intro u; case u|..]|]). } - revert H; generalize (dnorme d); clear d; intro d. - destruct d; intro H; rewrite H; clear H; [now simpl|]. - case (Z.of_int e); clear e; [|intro e..]. - - now simpl. - - simpl. - rewrite app_int_nil_r. - apply f_equal2; [|reflexivity]. - rewrite app_int_nil_r. - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - rewrite !Pos2Nat.inj_iter. - fold (Nat.iter (Pos.to_nat e) D0 Nil). - now rewrite of_int_iter_D0. - - simpl. - set (ai := match i with Pos _ => _ | _ => _ end). - rewrite app_int_nil_r. - case Nat.ltb_spec; intro Hei; simpl. - + rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. - rewrite Nat2Z.inj_sub; [|now apply le_Sn_le]. - rewrite Z.sub_sub_distr, Z.sub_diag; simpl. - rewrite positive_nat_Z; simpl. - now revert Hei; unfold ai; case i; clear i ai; intros i Hei; simpl; - (rewrite app_del_tail_head; [|now apply le_Sn_le]). - + set (n := nb_digits _). - assert (H : (n = Pos.to_nat e - nb_digits ai + nb_digits ai)%nat). - { unfold n; induction (_ - _)%nat; [now simpl|]. - now rewrite Unsigned.nat_iter_S; simpl; rewrite IHn0. } - rewrite H; clear n H. - rewrite Nat2Z.inj_add, (Nat2Z.inj_sub _ _ Hei). - rewrite <-Z.sub_sub_distr, Z.sub_diag, Z.sub_0_r. - rewrite positive_nat_Z; simpl. - rewrite <-(DecimalZ.of_to (Z.of_int (app_int _ _))), DecimalZ.to_of. - rewrite <-(DecimalZ.of_to (Z.of_int i)), DecimalZ.to_of. - apply f_equal2; [|reflexivity]; apply f_equal. - now unfold ai; case i; clear i ai Hei; intro i; - (induction (_ - _)%nat; [|rewrite <-IHn]). + split. apply of_inj. intros E. rewrite <- of_decimal_dnorm, E. + apply of_decimal_dnorm. Qed. diff --git a/theories/Numbers/DecimalR.v b/theories/Numbers/DecimalR.v new file mode 100644 index 0000000000..9b65a7dc20 --- /dev/null +++ b/theories/Numbers/DecimalR.v @@ -0,0 +1,312 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * DecimalR + + Proofs that conversions between decimal numbers and [R] + are bijections. *) + +Require Import Decimal DecimalFacts DecimalPos DecimalZ DecimalQ Rdefinitions. + +Lemma of_IQmake_to_decimal num den : + match IQmake_to_decimal num den with + | None => True + | Some (DecimalExp _ _ _) => False + | Some (Decimal i f) => + of_decimal (Decimal i f) = IRQ (QArith_base.Qmake num den) + end. +Proof. + unfold IQmake_to_decimal. + case (Pos.eq_dec den 1); [now intros->|intro Hden]. + assert (Hf : match QArith_base.IQmake_to_decimal num den with + | Some (Decimal i f) => f <> Nil + | _ => True + end). + { unfold QArith_base.IQmake_to_decimal; simpl. + generalize (Unsigned.nztail_to_uint den). + case Decimal.nztail as [den' e_den']. + case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'. + case den'; [ |now simpl..]; clear den'. + case e_den' as [|e_den']; [now simpl; intros H _; apply Hden; injection H|]. + intros _. + case Nat.ltb_spec; intro He_den'. + - apply del_head_nonnil. + revert He_den'; case nb_digits as [|n]; [now simpl|]. + now intro H; simpl; apply le_lt_n_Sm, Nat.le_sub_l. + - apply nb_digits_n0. + now rewrite nb_digits_iter_D0, Nat.sub_add. } + replace (match den with 1%positive => _ | _ => _ end) + with (QArith_base.IQmake_to_decimal num den); [|now revert Hden; case den]. + generalize (of_IQmake_to_decimal num den). + case QArith_base.IQmake_to_decimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + unfold of_decimal; simpl. + intro H; injection H; clear H; intros <-. + intro H; generalize (f_equal QArith_base.IZ_to_Z H); clear H. + rewrite !IZ_to_Z_IZ_of_Z; intro H; injection H; clear H; intros<-. + now revert Hf; case f. +Qed. + +Lemma of_to (q:IR) : forall d, to_decimal q = Some d -> of_decimal d = q. +Proof. + intro d. + case q as [z|q|r r'|r r']; simpl. + - case z as [z p| |p|p]. + + now simpl. + + now simpl; intro H; injection H; clear H; intros<-. + + simpl; intro H; injection H; clear H; intros<-. + now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to. + + simpl; intro H; injection H; clear H; intros<-. + now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to. + - case q as [num den]. + generalize (of_IQmake_to_decimal num den). + case IQmake_to_decimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + now intros H H'; injection H'; intros<-. + - case r as [z|q| |]; [|case q as[num den]|now simpl..]; + (case r' as [z'| | |]; [|now simpl..]); + (case z' as [p e| | |]; [|now simpl..]). + + case (Z.eq_dec p 10); [intros->|intro Hp]. + 2:{ revert Hp; case p; [now simpl|intro d0..]; + (case d0; [intro d1..|]; [now simpl| |now simpl]; + case d1; [intro d2..|]; [|now simpl..]; + case d2; [intro d3..|]; [now simpl| |now simpl]; + now case d3). } + case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-. + * now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to. + * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl. + now rewrite Unsigned.of_to. + * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl. + now rewrite Unsigned.of_to. + + case (Z.eq_dec p 10); [intros->|intro Hp]. + 2:{ revert Hp; case p; [now simpl|intro d0..]; + (case d0; [intro d1..|]; [now simpl| |now simpl]; + case d1; [intro d2..|]; [|now simpl..]; + case d2; [intro d3..|]; [now simpl| |now simpl]; + now case d3). } + generalize (of_IQmake_to_decimal num den). + case IQmake_to_decimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros H H'; injection H'; clear H'; intros<-. + unfold of_decimal; simpl. + change (match f with Nil => _ | _ => _ end) with (of_decimal (Decimal i f)). + rewrite H; clear H. + now unfold Z.of_uint; rewrite Unsigned.of_to. + - case r as [z|q| |]; [|case q as[num den]|now simpl..]; + (case r' as [z'| | |]; [|now simpl..]); + (case z' as [p e| | |]; [|now simpl..]). + + case (Z.eq_dec p 10); [intros->|intro Hp]. + 2:{ revert Hp; case p; [now simpl|intro d0..]; + (case d0; [intro d1..|]; [now simpl| |now simpl]; + case d1; [intro d2..|]; [|now simpl..]; + case d2; [intro d3..|]; [now simpl| |now simpl]; + now case d3). } + case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-. + * now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to. + * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl. + now rewrite Unsigned.of_to. + * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl. + now rewrite Unsigned.of_to. + + case (Z.eq_dec p 10); [intros->|intro Hp]. + 2:{ revert Hp; case p; [now simpl|intro d0..]; + (case d0; [intro d1..|]; [now simpl| |now simpl]; + case d1; [intro d2..|]; [|now simpl..]; + case d2; [intro d3..|]; [now simpl| |now simpl]; + now case d3). } + generalize (of_IQmake_to_decimal num den). + case IQmake_to_decimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros H H'; injection H'; clear H'; intros<-. + unfold of_decimal; simpl. + change (match f with Nil => _ | _ => _ end) with (of_decimal (Decimal i f)). + rewrite H; clear H. + now unfold Z.of_uint; rewrite Unsigned.of_to. +Qed. + +Lemma to_of (d:decimal) : to_decimal (of_decimal d) = Some (dnorm d). +Proof. + case d as [i f|i f e]. + - unfold of_decimal; simpl. + case (uint_eq_dec f Nil); intro Hf. + + rewrite Hf; clear f Hf. + unfold to_decimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + + set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_decimal; simpl. + unfold IQmake_to_decimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_decimal, n; simpl. + rewrite nztail_to_uint_pow10. + clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite DecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + * rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + * rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. + - unfold of_decimal; simpl. + rewrite <-(DecimalZ.to_of e). + case (Z.of_int e); clear e; [|intro e..]; simpl. + + case (uint_eq_dec f Nil); intro Hf. + * rewrite Hf; clear f Hf. + unfold to_decimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + * set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_decimal; simpl. + unfold IQmake_to_decimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_decimal, n; simpl. + rewrite nztail_to_uint_pow10. + clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite DecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + -- rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + -- rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. + + set (i' := match i with Pos _ => _ | _ => _ end). + set (m := match Pos.to_uint e with Nil => _ | _ => _ end). + replace m with (DecimalExp i' f (Pos (Pos.to_uint e))). + 2:{ unfold m; generalize (Unsigned.to_uint_nonzero e). + now case Pos.to_uint; [|intro u; case u|..]. } + unfold i'; clear i' m. + case (uint_eq_dec f Nil); intro Hf. + * rewrite Hf; clear f Hf. + unfold to_decimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + * set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_decimal; simpl. + unfold IQmake_to_decimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_decimal, n; simpl. + rewrite nztail_to_uint_pow10. + clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite DecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + -- rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + -- rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. + + case (uint_eq_dec f Nil); intro Hf. + * rewrite Hf; clear f Hf. + unfold to_decimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + * set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_decimal; simpl. + unfold IQmake_to_decimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_decimal, n; simpl. + rewrite nztail_to_uint_pow10. + clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite DecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + -- rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + -- rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. +Qed. + +(** Some consequences *) + +Lemma to_decimal_inj q q' : + to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'. +Proof. + intros Hnone EQ. + generalize (of_to q) (of_to q'). + rewrite <-EQ. + revert Hnone; case to_decimal; [|now simpl]. + now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). +Qed. + +Lemma to_decimal_surj d : exists q, to_decimal q = Some (dnorm d). +Proof. + exists (of_decimal d). apply to_of. +Qed. + +Lemma of_decimal_dnorm d : of_decimal (dnorm d) = of_decimal d. +Proof. now apply to_decimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed. + +Lemma of_inj d d' : of_decimal d = of_decimal d' -> dnorm d = dnorm d'. +Proof. + intro H. + apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end) + (Some (dnorm d)) (Some (dnorm d'))). + now rewrite <- !to_of, H. +Qed. + +Lemma of_iff d d' : of_decimal d = of_decimal d' <-> dnorm d = dnorm d'. +Proof. + split. apply of_inj. intros E. rewrite <- of_decimal_dnorm, E. + apply of_decimal_dnorm. +Qed. diff --git a/theories/Numbers/DecimalZ.v b/theories/Numbers/DecimalZ.v index 69d8073fc7..faaf8a3932 100644 --- a/theories/Numbers/DecimalZ.v +++ b/theories/Numbers/DecimalZ.v @@ -79,9 +79,11 @@ Qed. Lemma of_uint_iter_D0 d n : Z.of_uint (app d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 10) (Z.of_uint d). Proof. - unfold Z.of_uint. - unfold app; rewrite <-rev_revapp. - rewrite Unsigned.of_lu_rev, Unsigned.of_lu_revapp. + rewrite <-(rev_rev (app _ _)), <-(of_list_to_list (rev (app _ _))). + rewrite rev_spec, app_spec, List.rev_app_distr. + rewrite <-!rev_spec, <-app_spec, of_list_to_list. + unfold Z.of_uint; rewrite Unsigned.of_lu_rev. + unfold app; rewrite Unsigned.of_lu_revapp, !rev_rev. rewrite <-!Unsigned.of_lu_rev, !rev_rev. assert (H' : Pos.of_uint (Nat.iter n D0 Nil) = 0%N). { now induction n; [|rewrite Unsigned.nat_iter_S]. } @@ -100,3 +102,22 @@ Proof. - rewrite of_uint_iter_D0; induction n; [now simpl|]. rewrite !Unsigned.nat_iter_S, <-IHn; ring. Qed. + +Lemma nztail_to_uint_pow10 n : + Decimal.nztail (Pos.to_uint (Nat.iter n (Pos.mul 10) 1%positive)) + = (D1 Nil, n). +Proof. + case n as [|n]; [now simpl|]. + rewrite <-(Nat2Pos.id (S n)); [|now simpl]. + generalize (Pos.of_nat (S n)); clear n; intro p. + induction (Pos.to_nat p); [now simpl|]. + rewrite Unsigned.nat_iter_S. + unfold Pos.to_uint. + change (Pos.to_little_uint _) + with (Unsigned.to_lu (10 * N.pos (Nat.iter n (Pos.mul 10) 1%positive))). + rewrite Unsigned.to_ldec_tenfold. + revert IHn; unfold Pos.to_uint. + unfold Decimal.nztail; rewrite !rev_rev; simpl. + set (f'' := _ (Pos.to_little_uint _)). + now case f''; intros r n' H; inversion H. +Qed. diff --git a/theories/Numbers/HexadecimalFacts.v b/theories/Numbers/HexadecimalFacts.v index 7328b2303d..c624b4e6b9 100644 --- a/theories/Numbers/HexadecimalFacts.v +++ b/theories/Numbers/HexadecimalFacts.v @@ -10,136 +10,437 @@ (** * HexadecimalFacts : some facts about Hexadecimal numbers *) -Require Import Hexadecimal Arith. +Require Import Hexadecimal Arith ZArith. + +Variant digits := + | d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9 + | da | db | dc | dd | de | df. + +Fixpoint to_list (u : uint) : list digits := + match u with + | Nil => nil + | D0 u => cons d0 (to_list u) + | D1 u => cons d1 (to_list u) + | D2 u => cons d2 (to_list u) + | D3 u => cons d3 (to_list u) + | D4 u => cons d4 (to_list u) + | D5 u => cons d5 (to_list u) + | D6 u => cons d6 (to_list u) + | D7 u => cons d7 (to_list u) + | D8 u => cons d8 (to_list u) + | D9 u => cons d9 (to_list u) + | Da u => cons da (to_list u) + | Db u => cons db (to_list u) + | Dc u => cons dc (to_list u) + | Dd u => cons dd (to_list u) + | De u => cons de (to_list u) + | Df u => cons df (to_list u) + end. + +Fixpoint of_list (l : list digits) : uint := + match l with + | nil => Nil + | cons d0 l => D0 (of_list l) + | cons d1 l => D1 (of_list l) + | cons d2 l => D2 (of_list l) + | cons d3 l => D3 (of_list l) + | cons d4 l => D4 (of_list l) + | cons d5 l => D5 (of_list l) + | cons d6 l => D6 (of_list l) + | cons d7 l => D7 (of_list l) + | cons d8 l => D8 (of_list l) + | cons d9 l => D9 (of_list l) + | cons da l => Da (of_list l) + | cons db l => Db (of_list l) + | cons dc l => Dc (of_list l) + | cons dd l => Dd (of_list l) + | cons de l => De (of_list l) + | cons df l => Df (of_list l) + end. -Scheme Equality for uint. +Lemma of_list_to_list u : of_list (to_list u) = u. +Proof. now induction u; [|simpl; rewrite IHu..]. Qed. -Scheme Equality for int. +Lemma to_list_of_list l : to_list (of_list l) = l. +Proof. now induction l as [|h t IHl]; [|case h; simpl; rewrite IHl]. Qed. -Lemma rev_revapp d d' : - rev (revapp d d') = revapp d' d. +Lemma to_list_inj u u' : to_list u = to_list u' -> u = u'. Proof. - revert d'. induction d; simpl; intros; now rewrite ?IHd. + now intro H; rewrite <-(of_list_to_list u), <-(of_list_to_list u'), H. Qed. -Lemma rev_rev d : rev (rev d) = d. +Lemma of_list_inj u u' : of_list u = of_list u' -> u = u'. Proof. - apply rev_revapp. + now intro H; rewrite <-(to_list_of_list u), <-(to_list_of_list u'), H. Qed. -Lemma revapp_rev_nil d : revapp (rev d) Nil = d. -Proof. now fold (rev (rev d)); rewrite rev_rev. Qed. +Lemma nb_digits_spec u : nb_digits u = length (to_list u). +Proof. now induction u; [|simpl; rewrite IHu..]. Qed. -Lemma app_nil_r d : app d Nil = d. -Proof. now unfold app; rewrite revapp_rev_nil. Qed. +Fixpoint lnzhead l := + match l with + | nil => nil + | cons d l' => + match d with + | d0 => lnzhead l' + | _ => l + end + end. -Lemma app_int_nil_r d : app_int d Nil = d. -Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed. +Lemma nzhead_spec u : to_list (nzhead u) = lnzhead (to_list u). +Proof. now induction u; [|simpl; rewrite IHu|..]. Qed. + +Definition lzero := cons d0 nil. + +Definition lunorm l := + match lnzhead l with + | nil => lzero + | d => d + end. + +Lemma unorm_spec u : to_list (unorm u) = lunorm (to_list u). +Proof. now unfold unorm, lunorm; rewrite <-nzhead_spec; case (nzhead u). Qed. + +Lemma revapp_spec d d' : + to_list (revapp d d') = List.rev_append (to_list d) (to_list d'). +Proof. now revert d'; induction d; intro d'; [|simpl; rewrite IHd..]. Qed. + +Lemma rev_spec d : to_list (rev d) = List.rev (to_list d). +Proof. now unfold rev; rewrite revapp_spec, List.rev_alt; simpl. Qed. + +Lemma app_spec d d' : + to_list (app d d') = Datatypes.app (to_list d) (to_list d'). +Proof. + unfold app. + now rewrite revapp_spec, List.rev_append_rev, rev_spec, List.rev_involutive. +Qed. -Lemma revapp_revapp_1 d d' d'' : - nb_digits d <= 1 -> - revapp (revapp d d') d'' = revapp d' (revapp d d''). +Definition lnztail l := + let fix aux l_rev := + match l_rev with + | cons d0 l_rev => let (r, n) := aux l_rev in pair r (S n) + | _ => pair l_rev O + end in + let (r, n) := aux (List.rev l) in pair (List.rev r) n. + +Lemma nztail_spec d : + let (r, n) := nztail d in + let (r', n') := lnztail (to_list d) in + to_list r = r' /\ n = n'. Proof. - now case d; clear d; intro d; - [|case d; clear d; intro d; - [|simpl; case nb_digits; [|intros n]; intros Hn; exfalso; - [apply (Nat.nle_succ_diag_l _ Hn)| - apply (Nat.nle_succ_0 _ (le_S_n _ _ Hn))]..]..]. + unfold nztail, lnztail. + set (f := fix aux d_rev := match d_rev with + | D0 d_rev => let (r, n) := aux d_rev in (r, S n) + | _ => (d_rev, 0) end). + set (f' := fix aux (l_rev : list digits) : list digits * nat := + match l_rev with + | cons d0 l_rev => let (r, n) := aux l_rev in (r, S n) + | _ => (l_rev, 0) + end). + rewrite <-(of_list_to_list (rev d)), rev_spec. + induction (List.rev _) as [|h t IHl]; [now simpl|]. + case h; simpl; [|now rewrite rev_spec; simpl; rewrite to_list_of_list..]. + now revert IHl; case f; intros r n; case f'; intros r' n' [-> ->]. Qed. -Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d. -Proof. now case d; [|intros d' _; apply Nat.lt_0_succ..]. Qed. +Lemma del_head_spec_0 d : del_head 0 d = d. +Proof. now simpl. Qed. -Lemma nb_digits_revapp d d' : - nb_digits (revapp d d') = nb_digits d + nb_digits d'. +Lemma del_head_spec_small n d : + n <= length (to_list d) -> to_list (del_head n d) = List.skipn n (to_list d). Proof. - now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..]. + revert d; induction n as [|n IHn]; intro d; [now simpl|]. + now case d; [|intros d' H; apply IHn, le_S_n..]. Qed. -Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u. -Proof. now unfold rev; rewrite nb_digits_revapp. Qed. +Lemma del_head_spec_large n d : length (to_list d) < n -> del_head n d = zero. +Proof. + revert d; induction n; intro d; [now case d|]. + now case d; [|intro d'; simpl; intro H; rewrite (IHn _ (lt_S_n _ _ H))..]. +Qed. -Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u. -Proof. now induction u; [|apply le_S|..]. Qed. +Lemma nb_digits_0 d : nb_digits d = 0 -> d = Nil. +Proof. + rewrite nb_digits_spec, <-(of_list_to_list d). + now case (to_list d) as [|h t]; [|rewrite to_list_of_list]. +Qed. + +Lemma nb_digits_n0 d : nb_digits d <> 0 -> d <> Nil. +Proof. now case d; [|intros u _..]. Qed. Lemma nb_digits_iter_D0 n d : nb_digits (Nat.iter n D0 d) = n + nb_digits d. Proof. now induction n; simpl; [|rewrite IHn]. Qed. -Fixpoint nth n u := - match n with - | O => - match u with - | Nil => Nil - | D0 d => D0 Nil - | D1 d => D1 Nil - | D2 d => D2 Nil - | D3 d => D3 Nil - | D4 d => D4 Nil - | D5 d => D5 Nil - | D6 d => D6 Nil - | D7 d => D7 Nil - | D8 d => D8 Nil - | D9 d => D9 Nil - | Da d => Da Nil - | Db d => Db Nil - | Dc d => Dc Nil - | Dd d => Dd Nil - | De d => De Nil - | Df d => Df Nil - end - | S n => - match u with - | Nil => Nil - | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d - | Da d | Db d | Dc d | Dd d | De d | Df d => - nth n d - end - end. +Lemma length_lnzhead l : length (lnzhead l) <= length l. +Proof. now induction l as [|h t IHl]; [|case h; [apply le_S|..]]. Qed. + +Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u. +Proof. now induction u; [|apply le_S|..]. Qed. -Lemma nb_digits_nth n u : nb_digits (nth n u) <= 1. -Proof. - revert u; induction n. - - now intro u; case u; [apply Nat.le_0_1|..]. - - intro u; case u; [apply Nat.le_0_1|intro u'; apply IHn..]. -Qed. - -Lemma nth_revapp_r n d d' : - nb_digits d <= n -> - nth n (revapp d d') = nth (n - nb_digits d) d'. -Proof. - revert d d'; induction n; intro d. - - now case d; intro d'; - [case d'|intros d'' H; exfalso; revert H; apply Nat.nle_succ_0..]. - - now induction d; - [intro d'; case d'| - intros d' H; - simpl revapp; rewrite IHd; [|now apply le_Sn_le]; - rewrite Nat.sub_succ_l; [|now apply le_S_n]; - simpl; rewrite <-(IHn _ _ (le_S_n _ _ H))..]. -Qed. - -Lemma nth_revapp_l n d d' : - n < nb_digits d -> - nth n (revapp d d') = nth (nb_digits d - n - 1) d. -Proof. - revert d d'; induction n; intro d. - - rewrite Nat.sub_0_r. - now induction d; - [|intros d' _; simpl revapp; - revert IHd; case d; clear d; [|intro d..]; intro IHd; - [|rewrite IHd; [simpl nb_digits; rewrite (Nat.sub_succ_l _ (S _))|]; - [|apply le_n_S, Nat.le_0_l..]..]..]. - - now induction d; - [|intros d' H; - simpl revapp; simpl nb_digits; - simpl in H; generalize (lt_S_n _ _ H); clear H; intro H; - case (le_lt_eq_dec _ _ H); clear H; intro H; - [rewrite (IHd _ H), Nat.sub_succ_l; - [rewrite Nat.sub_succ_l; [|apply Nat.le_add_le_sub_r]| - apply le_Sn_le]| - rewrite nth_revapp_r; rewrite <-H; - [rewrite Nat.sub_succ, Nat.sub_succ_l; [rewrite !Nat.sub_diag|]|]]..]. +Lemma unorm_nzhead u : nzhead u <> Nil -> unorm u = nzhead u. +Proof. now unfold unorm; case nzhead. Qed. + +Lemma nb_digits_unorm u : u <> Nil -> nb_digits (unorm u) <= nb_digits u. +Proof. + intro Hu; case (uint_eq_dec (nzhead u) Nil). + { unfold unorm; intros ->; simpl. + now revert Hu; case u; [|intros u' _; apply le_n_S, Nat.le_0_l..]. } + intro H; rewrite (unorm_nzhead _ H); apply nb_digits_nzhead. +Qed. + +Lemma nb_digits_rev d : nb_digits (rev d) = nb_digits d. +Proof. now rewrite !nb_digits_spec, rev_spec, List.rev_length. Qed. + +Lemma nb_digits_del_head_sub d n : + n <= nb_digits d -> + nb_digits (del_head (nb_digits d - n) d) = n. +Proof. + rewrite !nb_digits_spec; intro Hn. + rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. + rewrite List.skipn_length, <-(Nat2Z.id (_ - _)). + rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. + rewrite (Nat2Z.inj_sub _ _ Hn). + rewrite Z.sub_sub_distr, Z.sub_diag; apply Nat2Z.id. +Qed. + +Lemma unorm_D0 u : unorm (D0 u) = unorm u. +Proof. reflexivity. Qed. + +Lemma app_nil_l d : app Nil d = d. +Proof. now simpl. Qed. + +Lemma app_nil_r d : app d Nil = d. +Proof. now apply to_list_inj; rewrite app_spec, List.app_nil_r. Qed. + +Lemma abs_app_int d d' : abs (app_int d d') = app (abs d) d'. +Proof. now case d. Qed. + +Lemma abs_norm d : abs (norm d) = unorm (abs d). +Proof. now case d as [u|u]; [|simpl; unfold unorm; case nzhead]. Qed. + +Lemma iter_D0_nzhead d : + Nat.iter (nb_digits d - nb_digits (nzhead d)) D0 (nzhead d) = d. +Proof. + induction d; [now simpl| |now rewrite Nat.sub_diag..]. + simpl nzhead; simpl nb_digits. + rewrite (Nat.sub_succ_l _ _ (nb_digits_nzhead _)). + now rewrite <-IHd at 4. +Qed. + +Lemma iter_D0_unorm d : + d <> Nil -> + Nat.iter (nb_digits d - nb_digits (unorm d)) D0 (unorm d) = d. +Proof. + case (uint_eq_dec (nzhead d) Nil); intro Hn. + { unfold unorm; rewrite Hn; simpl; intro H. + revert H Hn; induction d; [now simpl|intros _|now intros _..]. + case (uint_eq_dec d Nil); simpl; intros H Hn; [now rewrite H|]. + rewrite Nat.sub_0_r, (le_plus_minus 1 (nb_digits d)). + { now simpl; rewrite IHd. } + revert H; case d; [now simpl|intros u _; apply le_n_S, Nat.le_0_l..]. } + intros _; rewrite (unorm_nzhead _ Hn); apply iter_D0_nzhead. +Qed. + +Lemma nzhead_app_l d d' : + nb_digits d' < nb_digits (nzhead (app d d')) -> + nzhead (app d d') = app (nzhead d) d'. +Proof. + intro Hl; apply to_list_inj; revert Hl. + rewrite !nb_digits_spec, app_spec, !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]. + { now simpl; intro H; exfalso; revert H; apply le_not_lt, length_lnzhead. } + rewrite <-List.app_comm_cons. + now case h; [simpl; intro Hl; apply IHl|..]. +Qed. + +Lemma nzhead_app_r d d' : + nb_digits (nzhead (app d d')) <= nb_digits d' -> + nzhead (app d d') = nzhead d'. +Proof. + intro Hl; apply to_list_inj; revert Hl. + rewrite !nb_digits_spec, !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]; [now simpl|]. + rewrite <-List.app_comm_cons. + now case h; [| simpl; rewrite List.app_length; intro Hl; exfalso; revert Hl; + apply le_not_lt, le_plus_r..]. +Qed. + +Lemma nzhead_app_nil_r d d' : nzhead (app d d') = Nil -> nzhead d' = Nil. +Proof. +now intro H; generalize H; rewrite nzhead_app_r; [|rewrite H; apply Nat.le_0_l]. +Qed. + +Lemma nzhead_app_nil d d' : + nb_digits (nzhead (app d d')) <= nb_digits d' -> nzhead d = Nil. +Proof. + intro H; apply to_list_inj; revert H. + rewrite !nb_digits_spec, !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]; [now simpl|]. + now case h; [now simpl|..]; + simpl;intro H; exfalso; revert H; apply le_not_lt; + rewrite List.app_length; apply le_plus_r. +Qed. + +Lemma nzhead_app_nil_l d d' : nzhead (app d d') = Nil -> nzhead d = Nil. +Proof. + intro H; apply to_list_inj; generalize (f_equal to_list H); clear H. + rewrite !nzhead_spec, app_spec. + induction (to_list d) as [|h t IHl]; [now simpl|]. + now rewrite <-List.app_comm_cons; case h. +Qed. + +Lemma unorm_app_zero d d' : + nb_digits (unorm (app d d')) <= nb_digits d' -> unorm d = zero. +Proof. + unfold unorm. + case (uint_eq_dec (nzhead (app d d')) Nil). + { now intro Hn; rewrite Hn, (nzhead_app_nil_l _ _ Hn). } + intro H; fold (unorm (app d d')); rewrite (unorm_nzhead _ H); intro H'. + case (uint_eq_dec (nzhead d) Nil); [now intros->|]. + intro H''; fold (unorm d); rewrite (unorm_nzhead _ H''). + exfalso; apply H''; revert H'; apply nzhead_app_nil. +Qed. + +Lemma app_int_nil_r d : app_int d Nil = d. +Proof. + now case d; intro d'; simpl; + rewrite <-(of_list_to_list (app _ _)), app_spec; + rewrite List.app_nil_r, of_list_to_list. +Qed. + +Lemma unorm_app_l d d' : + nb_digits d' < nb_digits (unorm (app d d')) -> + unorm (app d d') = app (unorm d) d'. +Proof. + case (uint_eq_dec d' Nil); [now intros->; rewrite !app_nil_r|intro Hd']. + case (uint_eq_dec (nzhead (app d d')) Nil). + { unfold unorm; intros->; simpl; intro H; exfalso; revert H; apply le_not_lt. + now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. } + intro Ha; rewrite (unorm_nzhead _ Ha). + intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn). + rewrite !nb_digits_spec, app_spec, List.app_length. + case (uint_eq_dec (nzhead d) Nil). + { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. } + now intro H; rewrite (unorm_nzhead _ H). +Qed. + +Lemma unorm_app_r d d' : + nb_digits (unorm (app d d')) <= nb_digits d' -> + unorm (app d d') = unorm d'. +Proof. + case (uint_eq_dec (nzhead (app d d')) Nil). + { now unfold unorm; intro H; rewrite H, (nzhead_app_nil_r _ _ H). } + intro Ha; rewrite (unorm_nzhead _ Ha). + case (uint_eq_dec (nzhead d') Nil). + { now intros H H'; exfalso; apply Ha; rewrite nzhead_app_r. } + intro Hd'; rewrite (unorm_nzhead _ Hd'); apply nzhead_app_r. +Qed. + +Lemma norm_app_int d d' : + nb_digits d' < nb_digits (unorm (app (abs d) d')) -> + norm (app_int d d') = app_int (norm d) d'. +Proof. + case (uint_eq_dec d' Nil); [now intros->; rewrite !app_int_nil_r|intro Hd']. + case d as [d|d]; [now simpl; intro H; apply f_equal, unorm_app_l|]. + simpl; unfold unorm. + case (uint_eq_dec (nzhead (app d d')) Nil). + { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt. + now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. } + set (m := match nzhead _ with Nil => _ | _ => _ end). + intro Ha. + replace m with (nzhead (app d d')). + 2:{ now unfold m; revert Ha; case nzhead. } + intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn). + case (uint_eq_dec (app (nzhead d) d') Nil). + { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt, Nat.le_0_l. } + clear m; set (m := match app _ _ with Nil => _ | _ => _ end). + intro Ha'. + replace m with (Neg (app (nzhead d) d')); [|now unfold m; revert Ha'; case app]. + case (uint_eq_dec (nzhead d) Nil). + { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. } + clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). + intro Hd. + now replace m with (Neg (nzhead d)); [|unfold m; revert Hd; case nzhead]. +Qed. + +Lemma del_head_nb_digits d : del_head (nb_digits d) d = Nil. +Proof. + apply to_list_inj. + rewrite nb_digits_spec, del_head_spec_small; [|now simpl]. + now rewrite List.skipn_all. +Qed. + +Lemma del_tail_nb_digits d : del_tail (nb_digits d) d = Nil. +Proof. now unfold del_tail; rewrite <-nb_digits_rev, del_head_nb_digits. Qed. + +Lemma del_head_app n d d' : + n <= nb_digits d -> del_head n (app d d') = app (del_head n d) d'. +Proof. + rewrite nb_digits_spec; intro Hn. + apply to_list_inj. + rewrite del_head_spec_small. + 2:{ now rewrite app_spec, List.app_length; apply le_plus_trans. } + rewrite !app_spec, (del_head_spec_small _ _ Hn). + rewrite List.skipn_app. + now rewrite (proj2 (Nat.sub_0_le _ _) Hn). +Qed. + +Lemma del_tail_app n d d' : + n <= nb_digits d' -> del_tail n (app d d') = app d (del_tail n d'). +Proof. + rewrite nb_digits_spec; intro Hn. + unfold del_tail. + rewrite <-(of_list_to_list (rev (app d d'))), rev_spec, app_spec. + rewrite List.rev_app_distr, <-!rev_spec, <-app_spec, of_list_to_list. + rewrite del_head_app; [|now rewrite nb_digits_spec, rev_spec, List.rev_length]. + apply to_list_inj. + rewrite rev_spec, !app_spec, !rev_spec. + now rewrite List.rev_app_distr, List.rev_involutive. +Qed. + +Lemma del_tail_app_int n d d' : + n <= nb_digits d' -> del_tail_int n (app_int d d') = app_int d (del_tail n d'). +Proof. now case d as [d|d]; simpl; intro H; rewrite del_tail_app. Qed. + +Lemma app_del_tail_head n (d:uint) : + n <= nb_digits d -> app (del_tail n d) (del_head (nb_digits d - n) d) = d. +Proof. + rewrite nb_digits_spec; intro Hn; unfold del_tail. + rewrite <-(of_list_to_list (app _ _)), app_spec, rev_spec. + rewrite del_head_spec_small; [|now rewrite rev_spec, List.rev_length]. + rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. + rewrite rev_spec. + set (n' := _ - n). + assert (Hn' : n = length (to_list d) - n'). + { now apply plus_minus; rewrite Nat.add_comm; symmetry; apply le_plus_minus_r. } + now rewrite Hn', <-List.firstn_skipn_rev, List.firstn_skipn, of_list_to_list. +Qed. + +Lemma app_int_del_tail_head n (d:int) : + n <= nb_digits (abs d) -> + app_int (del_tail_int n d) (del_head (nb_digits (abs d) - n) (abs d)) = d. +Proof. now case d; clear d; simpl; intros u Hu; rewrite app_del_tail_head. Qed. + +Lemma del_head_app_int_exact i f : + nb_digits f < nb_digits (unorm (app (abs i) f)) -> + del_head (nb_digits (unorm (app (abs i) f)) - nb_digits f) (unorm (app (abs i) f)) = f. +Proof. + simpl; intro Hnb; generalize Hnb; rewrite (unorm_app_l _ _ Hnb); clear Hnb. + replace (_ - _) with (nb_digits (unorm (abs i))). + - now rewrite del_head_app; [rewrite del_head_nb_digits|]. + - rewrite !nb_digits_spec, app_spec, List.app_length. + now rewrite Nat.add_comm, minus_plus. +Qed. + +Lemma del_tail_app_int_exact i f : + nb_digits f < nb_digits (unorm (app (abs i) f)) -> + del_tail_int (nb_digits f) (norm (app_int i f)) = norm i. +Proof. + simpl; intro Hnb. + rewrite (norm_app_int _ _ Hnb). + rewrite del_tail_app_int; [|now simpl]. + now rewrite del_tail_nb_digits, app_int_nil_r. Qed. (** Normalization on little-endian numbers *) @@ -193,6 +494,9 @@ Proof. apply nzhead_revapp. Qed. +Lemma rev_rev d : rev (rev d) = d. +Proof. now apply to_list_inj; rewrite !rev_spec, List.rev_involutive. Qed. + Lemma rev_nztail_rev d : rev (nztail (rev d)) = nzhead d. Proof. @@ -247,47 +551,128 @@ Proof. unfold unorm. now destruct nzhead. Qed. -Lemma unorm_D0 u : unorm (D0 u) = unorm u. -Proof. reflexivity. Qed. - Lemma unorm_iter_D0 n u : unorm (Nat.iter n D0 u) = unorm u. Proof. now induction n. Qed. -Lemma nb_digits_unorm u : - u <> Nil -> nb_digits (unorm u) <= nb_digits u. +Lemma del_head_nonnil n u : + n < nb_digits u -> del_head n u <> Nil. Proof. - case u; clear u; [now simpl|intro u..]; [|now simpl..]. - intros _; unfold unorm. - case_eq (nzhead (D0 u)); [|now intros u' <-; apply nb_digits_nzhead..]. - intros _; apply le_n_S, Nat.le_0_l. + now revert n; induction u; intro n; + [|case n; [|intro n'; simpl; intro H; apply IHu, lt_S_n]..]. Qed. -Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d. +Lemma del_tail_nonnil n u : + n < nb_digits u -> del_tail n u <> Nil. +Proof. + unfold del_tail. + rewrite <-nb_digits_rev. + generalize (rev u); clear u; intro u. + intros Hu H. + generalize (rev_nil_inv _ H); clear H. + now apply del_head_nonnil. +Qed. + +Lemma nzhead_involutive d : nzhead (nzhead d) = nzhead d. Proof. now induction d. Qed. +#[deprecated(since="8.13",note="Use nzhead_involutive instead.")] +Notation nzhead_invol := nzhead_involutive (only parsing). -Lemma nztail_invol d : nztail (nztail d) = nztail d. +Lemma nztail_involutive d : nztail (nztail d) = nztail d. Proof. rewrite <-(rev_rev (nztail _)), <-(rev_rev (nztail d)), <-(rev_rev d). - now rewrite !rev_nztail_rev, nzhead_invol. + now rewrite !rev_nztail_rev, nzhead_involutive. Qed. +#[deprecated(since="8.13",note="Use nztail_involutive instead.")] +Notation nztail_invol := nztail_involutive (only parsing). -Lemma unorm_invol d : unorm (unorm d) = unorm d. +Lemma unorm_involutive d : unorm (unorm d) = unorm d. Proof. unfold unorm. destruct (nzhead d) eqn:E; trivial. destruct (nzhead_nonzero _ _ E). Qed. +#[deprecated(since="8.13",note="Use unorm_involutive instead.")] +Notation unorm_invol := unorm_involutive (only parsing). -Lemma norm_invol d : norm (norm d) = norm d. +Lemma norm_involutive d : norm (norm d) = norm d. Proof. unfold norm. destruct d. - - f_equal. apply unorm_invol. + - f_equal. apply unorm_involutive. - destruct (nzhead d) eqn:E; auto. destruct (nzhead_nonzero _ _ E). Qed. +#[deprecated(since="8.13",note="Use norm_involutive instead.")] +Notation norm_invol := norm_involutive (only parsing). + +Lemma lnzhead_neq_d0_head l l' : ~(lnzhead l = cons d0 l'). +Proof. now induction l as [|h t Il]; [|case h]. Qed. + +Lemma lnzhead_head_nd0 h t : h <> d0 -> lnzhead (cons h t) = cons h t. +Proof. now case h. Qed. + +Lemma nzhead_del_tail_nzhead_eq n u : + nzhead u = u -> + n < nb_digits u -> + nzhead (del_tail n u) = del_tail n u. +Proof. + rewrite nb_digits_spec, <-List.rev_length. + intros Hu Hn. + apply to_list_inj; unfold del_tail. + rewrite nzhead_spec, rev_spec. + rewrite del_head_spec_small; [|now rewrite rev_spec; apply Nat.lt_le_incl]. + rewrite rev_spec. + rewrite List.skipn_rev, List.rev_involutive. + generalize (f_equal to_list Hu) Hn; rewrite nzhead_spec; intro Hu'. + case (to_list u) as [|h t]. + { simpl; intro H; exfalso; revert H; apply le_not_lt, Peano.le_0_n. } + intro Hn'; generalize (Nat.sub_gt _ _ Hn'); rewrite List.rev_length. + case (_ - _); [now simpl|]; intros n' _. + rewrite List.firstn_cons, lnzhead_head_nd0; [now simpl|]. + intro Hh; revert Hu'; rewrite Hh; apply lnzhead_neq_d0_head. +Qed. + +Lemma nzhead_del_tail_nzhead n u : + n < nb_digits (nzhead u) -> + nzhead (del_tail n (nzhead u)) = del_tail n (nzhead u). +Proof. apply nzhead_del_tail_nzhead_eq, nzhead_involutive. Qed. + +Lemma unorm_del_tail_unorm n u : + n < nb_digits (unorm u) -> + unorm (del_tail n (unorm u)) = del_tail n (unorm u). +Proof. + case (uint_eq_dec (nzhead u) Nil). + - unfold unorm; intros->; case n; [now simpl|]; intro n'. + now simpl; intro H; exfalso; generalize (lt_S_n _ _ H). + - unfold unorm. + set (m := match nzhead u with Nil => zero | _ => _ end). + intros H. + replace m with (nzhead u). + + intros H'. + rewrite (nzhead_del_tail_nzhead _ _ H'). + now generalize (del_tail_nonnil _ _ H'); case del_tail. + + now unfold m; revert H; case nzhead. +Qed. + +Lemma norm_del_tail_int_norm n d : + n < nb_digits (match norm d with Pos d | Neg d => d end) -> + norm (del_tail_int n (norm d)) = del_tail_int n (norm d). +Proof. + case d; clear d; intros u; simpl. + - now intro H; simpl; rewrite unorm_del_tail_unorm. + - case (uint_eq_dec (nzhead u) Nil); intro Hu. + + now rewrite Hu; case n; [|intros n' Hn'; generalize (lt_S_n _ _ Hn')]. + + set (m := match nzhead u with Nil => Pos zero | _ => _ end). + replace m with (Neg (nzhead u)); [|now unfold m; revert Hu; case nzhead]. + unfold del_tail_int. + clear m Hu. + simpl. + intro H; generalize (del_tail_nonnil _ _ H). + rewrite (nzhead_del_tail_nzhead _ _ H). + now case del_tail. +Qed. Lemma nzhead_app_nzhead d d' : nzhead (app (nzhead d) d') = nzhead (app d d'). @@ -299,7 +684,7 @@ Proof. generalize (nzhead_revapp d d'). generalize (nzhead_revapp_0 (nztail d) d'). generalize (nzhead_revapp (nztail d) d'). - rewrite nztail_invol. + rewrite nztail_involutive. now case nztail; [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl) |intros d'' H _ H' _; rewrite H; [rewrite H'|]..]. @@ -336,5 +721,5 @@ Proof. |rewrite H'; unfold r; clear m r H']; unfold norm; rewrite rev_rev, <-Hd''; - rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..]. + rewrite nzhead_revapp; rewrite nztail_involutive; [|rewrite Hd'']..]. Qed. diff --git a/theories/Numbers/HexadecimalN.v b/theories/Numbers/HexadecimalN.v index f333e2b7f6..93ba82d14a 100644 --- a/theories/Numbers/HexadecimalN.v +++ b/theories/Numbers/HexadecimalN.v @@ -74,7 +74,7 @@ Proof. destruct (norm d) eqn:Hd; intros [= <-]. unfold N.to_hex_int. rewrite Unsigned.to_of. f_equal. revert Hd; destruct d; simpl. - - intros [= <-]. apply unorm_invol. + - intros [= <-]. apply unorm_involutive. - destruct (nzhead d); now intros [= <-]. Qed. @@ -93,7 +93,7 @@ Qed. Lemma of_int_norm d : N.of_hex_int (norm d) = N.of_hex_int d. Proof. - unfold N.of_hex_int. now rewrite norm_invol. + unfold N.of_hex_int. now rewrite norm_involutive. Qed. Lemma of_inj_pos d d' : diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v index b05184e821..94a14b90bd 100644 --- a/theories/Numbers/HexadecimalNat.v +++ b/theories/Numbers/HexadecimalNat.v @@ -289,7 +289,7 @@ Proof. destruct (norm d) eqn:Hd; intros [= <-]. unfold Nat.to_hex_int. rewrite Unsigned.to_of. f_equal. revert Hd; destruct d; simpl. - - intros [= <-]. apply unorm_invol. + - intros [= <-]. apply unorm_involutive. - destruct (nzhead d); now intros [= <-]. Qed. @@ -308,7 +308,7 @@ Qed. Lemma of_int_norm d : Nat.of_hex_int (norm d) = Nat.of_hex_int d. Proof. - unfold Nat.of_hex_int. now rewrite norm_invol. + unfold Nat.of_hex_int. now rewrite norm_involutive. Qed. Lemma of_inj_pos d d' : diff --git a/theories/Numbers/HexadecimalQ.v b/theories/Numbers/HexadecimalQ.v index 9bf43ceb88..a32019767c 100644 --- a/theories/Numbers/HexadecimalQ.v +++ b/theories/Numbers/HexadecimalQ.v @@ -16,442 +16,412 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ. Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith. -Lemma of_to (q:Q) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. +Lemma of_IQmake_to_hexadecimal num den : + match IQmake_to_hexadecimal num den with + | None => True + | Some (HexadecimalExp _ _ _) => False + | Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IQmake (IZ_of_Z num) den + end. +Proof. + unfold IQmake_to_hexadecimal. + generalize (Unsigned.nztail_to_hex_uint den). + case Hexadecimal.nztail; intros den' e_den'. + case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'. + case den'; [ |now simpl..]; clear den'. + case e_den' as [|e_den']; simpl; intro H; injection H; clear H; intros->. + { now unfold of_hexadecimal; simpl; rewrite app_int_nil_r, HexadecimalZ.of_to. } + replace (16 ^ _)%positive with (Nat.iter (S e_den') (Pos.mul 16) 1%positive). + 2:{ induction e_den' as [|n IHn]; [now simpl| ]. + now rewrite SuccNat2Pos.inj_succ, Pos.pow_succ_r, <-IHn. } + case Nat.ltb_spec; intro He_den'. + - unfold of_hexadecimal; simpl. + rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl]. + rewrite HexadecimalZ.of_to. + now rewrite nb_digits_del_head_sub; [|now apply Nat.lt_le_incl]. + - unfold of_hexadecimal; simpl. + rewrite nb_digits_iter_D0. + apply f_equal2. + + apply f_equal, HexadecimalZ.to_int_inj. + rewrite HexadecimalZ.to_of. + rewrite <-(HexadecimalZ.of_to num), HexadecimalZ.to_of. + case (Z.to_hex_int num); clear He_den' num; intro num; simpl. + * unfold app; simpl. + now rewrite unorm_D0, unorm_iter_D0, unorm_involutive. + * case (uint_eq_dec (nzhead num) Nil); [|intro Hn]. + { intros->; simpl; unfold app; simpl. + now rewrite unorm_D0, unorm_iter_D0. } + replace (match nzhead num with Nil => _ | _ => _ end) + with (Neg (nzhead num)); [|now revert Hn; case nzhead]. + simpl. + rewrite nzhead_iter_D0, nzhead_involutive. + now revert Hn; case nzhead. + + revert He_den'; case nb_digits as [|n]; [now simpl; rewrite Nat.add_0_r|]. + intro Hn. + rewrite Nat.add_succ_r, Nat.add_comm. + now rewrite <-le_plus_minus; [|apply le_S_n]. +Qed. + +Lemma IZ_of_Z_IZ_to_Z z z' : IZ_to_Z z = Some z' -> IZ_of_Z z' = z. +Proof. now case z as [| |p|p]; [|intro H; injection H; intros<-..]. Qed. + +Lemma of_IQmake_to_hexadecimal' num den : + match IQmake_to_hexadecimal' num den with + | None => True + | Some (HexadecimalExp _ _ _) => False + | Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IQmake num den + end. +Proof. + unfold IQmake_to_hexadecimal'. + case_eq (IZ_to_Z num); [intros num' Hnum'|now simpl]. + generalize (of_IQmake_to_hexadecimal num' den). + case IQmake_to_hexadecimal as [d|]; [|now simpl]. + case d as [i f|]; [|now simpl]. + now rewrite (IZ_of_Z_IZ_to_Z _ _ Hnum'). +Qed. + +Lemma of_to (q:IQ) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. Proof. - cut (match to_hexadecimal q with None => True | Some d => of_hexadecimal d = q end). - { now case to_hexadecimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. } - destruct q as (num, den). - unfold to_hexadecimal; simpl Qnum; simpl Qden. - generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint den). - case Hexadecimal.nztail; intros u n. - change 16%N with (2^4)%N; rewrite <-N.pow_mul_r. - change 4%N with (N.of_nat 4); rewrite <-Nnat.Nat2N.inj_mul. - change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul. - case u; clear u; try (intros; exact I); [| | |]; intro u; - (case u; clear u; [|intros; exact I..]). - - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc; rewrite N.mul_1_l. - case n. - + unfold of_hexadecimal, app_int, app, Z.to_hex_int; simpl. - intro H; inversion H as (H1); clear H H1. - case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_hex_uint pnum)))..]. - * rewrite rev_rev; simpl. - now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to. - * rewrite rev_rev; simpl. - now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to. - + clear n; intros n. - intro H; injection H; intros ->; clear H. - unfold of_hexadecimal. - rewrite DecimalZ.of_to. - simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. - now apply f_equal2; [rewrite app_int_nil_r, of_to|]. - - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc. - rewrite <-N.pow_succ_r', <-Nnat.Nat2N.inj_succ. - intro H; injection H; intros ->; clear H. - fold (4 * n)%nat. - change 1%Z with (Z.of_nat 1); rewrite <-Znat.Nat2Z.inj_add. - unfold of_hexadecimal. - rewrite DecimalZ.of_to. - simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. - now apply f_equal2; [rewrite app_int_nil_r, of_to|]. - - change 2%Z with (Z.of_nat 2); rewrite <-Znat.Nat2Z.inj_add. - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc. - change 4%N with (2^2)%N; rewrite <-N.pow_add_r. - change 2%N with (N.of_nat 2); rewrite <-Nnat.Nat2N.inj_add. - intro H; injection H; intros ->; clear H. - fold (4 * n)%nat. - unfold of_hexadecimal. - rewrite DecimalZ.of_to. - simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. - now apply f_equal2; [rewrite app_int_nil_r, of_to|]. - - change 3%Z with (Z.of_nat 3); rewrite <-Znat.Nat2Z.inj_add. - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc. - change 8%N with (2^3)%N; rewrite <-N.pow_add_r. - change 3%N with (N.of_nat 3); rewrite <-Nnat.Nat2N.inj_add. - intro H; injection H; intros ->; clear H. - fold (4 * n)%nat. - unfold of_hexadecimal. - rewrite DecimalZ.of_to. - simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. - now apply f_equal2; [rewrite app_int_nil_r, of_to|]. + intro d. + case q as [num den|q q'|q q']; simpl. + - generalize (of_IQmake_to_hexadecimal' num den). + case IQmake_to_hexadecimal' as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + now intros H H'; injection H'; clear H'; intros <-. + - case q as [num den| |]; [|now simpl..]. + case q' as [num' den'| |]; [|now simpl..]. + case num' as [z p| | |]; [|now simpl..]. + case (Z.eq_dec z 2); [intros->|]. + 2:{ case z; [now simpl| |now simpl]; intro pz'. + case pz'; [intros d0..| ]; [now simpl| |now simpl]. + now case d0. } + case (Pos.eq_dec den' 1%positive); [intros->|now case den']. + generalize (of_IQmake_to_hexadecimal' num den). + case IQmake_to_hexadecimal' as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros <-; clear num den. + intros H; injection H; clear H; intros<-. + unfold of_hexadecimal; simpl. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + - case q as [num den| |]; [|now simpl..]. + case q' as [num' den'| |]; [|now simpl..]. + case num' as [z p| | |]; [|now simpl..]. + case (Z.eq_dec z 2); [intros->|]. + 2:{ case z; [now simpl| |now simpl]; intro pz'. + case pz'; [intros d0..| ]; [now simpl| |now simpl]. + now case d0. } + case (Pos.eq_dec den' 1%positive); [intros->|now case den']. + generalize (of_IQmake_to_hexadecimal' num den). + case IQmake_to_hexadecimal' as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros <-; clear num den. + intros H; injection H; clear H; intros<-. + unfold of_hexadecimal; simpl. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. Qed. -(* normalize without fractional part, for instance norme 0x1.2p-1 is 0x12e-5 *) -Definition hnorme (d:hexadecimal) : hexadecimal := - let '(i, f, e) := - match d with - | Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil) - | HexadecimalExp i f e => (i, f, e) + +Definition dnorm (d:hexadecimal) : hexadecimal := + let norm_i i f := + match i with + | Pos i => Pos (unorm i) + | Neg i => match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end end in - let i := norm (app_int i f) in - let e := (Z.of_int e - 4 * Z.of_nat (nb_digits f))%Z in - match e with - | Z0 => Hexadecimal i Nil - | Zpos e => Hexadecimal (Pos.iter double i e) Nil - | Zneg _ => HexadecimalExp i Nil (Decimal.norm (Z.to_int e)) + match d with + | Hexadecimal i f => Hexadecimal (norm_i i f) f + | HexadecimalExp i f e => + match Decimal.norm e with + | Decimal.Pos Decimal.zero => Hexadecimal (norm_i i f) f + | e => HexadecimalExp (norm_i i f) f e + end end. -Lemma hnorme_spec d : - match hnorme d with - | Hexadecimal i Nil => i = norm i - | HexadecimalExp i Nil e => - i = norm i /\ e = Decimal.norm e /\ e <> Decimal.Pos Decimal.zero - | _ => False +Lemma dnorm_spec_i d : + let (i, f) := + match d with Hexadecimal i f => (i, f) | HexadecimalExp i f _ => (i, f) end in + let i' := match dnorm d with Hexadecimal i _ => i | HexadecimalExp i _ _ => i end in + match i with + | Pos i => i' = Pos (unorm i) + | Neg i => + (i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil)) + \/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil)) end. Proof. - case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl. - - case_eq (nb_digits f); [now simpl; rewrite norm_invol|]; intros nf Hnf. - split; [now simpl; rewrite norm_invol|]. - unfold Z.of_nat. - now rewrite <-!DecimalZ.to_of, !DecimalZ.of_to. - - set (e' := (_ - _)%Z). - case_eq e'; [|intro pe'..]; intro He'. - + now rewrite norm_invol. - + rewrite Pos2Nat.inj_iter. - set (ne' := Pos.to_nat pe'). - fold (Nat.iter ne' double (norm (app_int i f))). - induction ne'; [now simpl; rewrite norm_invol|]. - now rewrite Unsigned.nat_iter_S, <-double_norm, IHne', norm_invol. - + split; [now rewrite norm_invol|]. - split; [now rewrite DecimalFacts.norm_invol|]. - rewrite <-DecimalZ.to_of, DecimalZ.of_to. - change (Decimal.Pos _) with (Z.to_int 0). - now intro H; generalize (DecimalZ.to_int_inj _ _ H). + case d as [i f|i f e]; case i as [i|i]. + - now simpl. + - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha. + + rewrite Ha; right; split; [now simpl|split]. + * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha). + * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha). + + left; split; [now revert Ha; case nzhead|]. + case (uint_eq_dec (nzhead i) Nil). + * intro Hi; right; intro Hf; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + * now intro H; left. + - simpl; case (Decimal.norm e); clear e; intro e; [|now simpl]. + now case e; clear e; [|intro e..]; [|case e|..]. + - simpl. + set (m := match nzhead _ with Nil => _ | _ => _ end). + set (m' := match _ with Hexadecimal _ _ => _ | _ => _ end). + replace m' with m. + 2:{ unfold m'; case (Decimal.norm e); clear m' e; intro e; [|now simpl]. + now case e; clear e; [|intro e..]; [|case e|..]. } + unfold m; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha. + + rewrite Ha; right; split; [now simpl|split]. + * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha). + * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha). + + left; split; [now revert Ha; case nzhead|]. + case (uint_eq_dec (nzhead i) Nil). + * intro Hi; right; intro Hf; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + * now intro H; left. Qed. -Lemma hnorme_invol d : hnorme (hnorme d) = hnorme d. +Lemma dnorm_spec_f d : + let f := match d with Hexadecimal _ f => f | HexadecimalExp _ f _ => f end in + let f' := match dnorm d with Hexadecimal _ f => f | HexadecimalExp _ f _ => f end in + f' = f. +Proof. + case d as [i f|i f e]; [now simpl|]. + simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); [now intros->|intro He]. + set (i' := match i with Pos _ => _ | _ => _ end). + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). + replace m with (HexadecimalExp i' f (Decimal.norm e)); [now simpl|]. + unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. +Qed. + +Lemma dnorm_spec_e d : + match d, dnorm d with + | Hexadecimal _ _, Hexadecimal _ _ => True + | HexadecimalExp _ _ e, Hexadecimal _ _ => + Decimal.norm e = Decimal.Pos Decimal.zero + | HexadecimalExp _ _ e, HexadecimalExp _ _ e' => + e' = Decimal.norm e /\ e' <> Decimal.Pos Decimal.zero + | Hexadecimal _ _, HexadecimalExp _ _ _ => False + end. Proof. - case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl. - - case_eq (nb_digits f); [now simpl; rewrite app_int_nil_r, norm_invol|]. - intros nf Hnf. - unfold Z.of_nat. - simpl. - set (pnf := Pos.to_uint _). - set (nz := Decimal.nzhead pnf). - assert (Hnz : nz <> Decimal.Nil). - { unfold nz, pnf. - rewrite <-DecimalFacts.unorm_0. - rewrite <-DecimalPos.Unsigned.to_of. - rewrite DecimalPos.Unsigned.of_to. - change Decimal.zero with (N.to_uint 0). - now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). } - set (m := match nz with Decimal.Nil => _ | _ => _ end). - assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))). - { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. } - rewrite Hm; unfold pnf. - rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to. - simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. - rewrite Z.sub_0_r; simpl. - fold pnf; fold nz; fold m; rewrite Hm; unfold pnf. - rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to. - now rewrite app_int_nil_r, norm_invol. - - set (e' := (_ - _)%Z). - case_eq e'; [|intro pe'..]; intro Hpe'. - + now simpl; rewrite app_int_nil_r, norm_invol. - + simpl; rewrite app_int_nil_r. - apply f_equal2; [|reflexivity]. - rewrite Pos2Nat.inj_iter. - set (ne' := Pos.to_nat pe'). - fold (Nat.iter ne' double (norm (app_int i f))). - induction ne'; [now simpl; rewrite norm_invol|]. - now rewrite Unsigned.nat_iter_S, <-double_norm, IHne'. - + rewrite <-DecimalZ.to_of, !DecimalZ.of_to; simpl. - rewrite app_int_nil_r, norm_invol. - set (pnf := Pos.to_uint _). - set (nz := Decimal.nzhead pnf). - assert (Hnz : nz <> Decimal.Nil). - { unfold nz, pnf. - rewrite <-DecimalFacts.unorm_0. - rewrite <-DecimalPos.Unsigned.to_of. - rewrite DecimalPos.Unsigned.of_to. - change Decimal.zero with (N.to_uint 0). - now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). } - set (m := match nz with Decimal.Nil => _ | _ => _ end). - assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))). - { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. } - rewrite Hm; unfold pnf. - now rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to. + case d as [i f|i f e]; [now simpl|]. + simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); [now intros->|intro He]. + set (i' := match i with Pos _ => _ | _ => _ end). + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). + replace m with (HexadecimalExp i' f (Decimal.norm e)); [now simpl|]. + unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. Qed. -Lemma to_of (d:hexadecimal) : - to_hexadecimal (of_hexadecimal d) = Some (hnorme d). +Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm d. Proof. - unfold to_hexadecimal. - pose (t10 := fun y => (y~0~0~0~0)%positive). - assert (H : exists h e_den, - Hexadecimal.nztail (Pos.to_hex_uint (Qden (of_hexadecimal d))) - = (h, e_den) - /\ (h = D1 Nil \/ h = D2 Nil \/ h = D4 Nil \/ h = D8 Nil)). - { assert (H : forall p, - Hexadecimal.nztail (Pos.to_hex_uint (Pos.iter (Pos.mul 2) 1%positive p)) - = ((match (Pos.to_nat p) mod 4 with 0%nat => D1 | 1 => D2 | 2 => D4 | _ => D8 end)%nat Nil, - (Pos.to_nat p / 4)%nat)). - { intro p; clear d; rewrite Pos2Nat.inj_iter. - fold (Nat.iter (Pos.to_nat p) (Pos.mul 2) 1%positive). - set (n := Pos.to_nat p). - fold (Nat.iter n t10 1%positive). - set (nm4 := (n mod 4)%nat); set (nd4 := (n / 4)%nat). - rewrite (Nat.div_mod n 4); [|now simpl]. - unfold nm4, nd4; clear nm4 nd4. - generalize (Nat.mod_upper_bound n 4 ltac:(now simpl)). - generalize (n mod 4); generalize (n / 4)%nat. - intros d r Hr; clear p n. - induction d. - { simpl; revert Hr. - do 4 (case r; [now simpl|clear r; intro r]). - intro H; exfalso. - now do 4 (generalize (lt_S_n _ _ H); clear H; intro H). } - rewrite Nat.mul_succ_r, <-Nat.add_assoc, (Nat.add_comm 4), Nat.add_assoc. - rewrite (Nat.add_comm _ 4). - change (4 + _)%nat with (S (S (S (S (4 * d + r))))). - rewrite !Unsigned.nat_iter_S. - rewrite !Pos.mul_assoc. - unfold Pos.to_hex_uint. - change (2 * 2 * 2 * 2)%positive with 0x10%positive. - set (n := Nat.iter _ _ _). - change (Pos.to_little_hex_uint _) with (Unsigned.to_lu (16 * N.pos n)). - rewrite Unsigned.to_lhex_tenfold. - unfold Hexadecimal.nztail; rewrite rev_rev. - rewrite <-(rev_rev (Unsigned.to_lu _)). - set (m := _ (rev _)). - replace m with (let (r, n) := let (r, n) := m in (rev r, n) in (rev r, n)). - 2:{ now case m; intros r' n'; rewrite rev_rev. } - change (let (r, n) := m in (rev r, n)) - with (Hexadecimal.nztail (Pos.to_hex_uint n)). - now unfold n; rewrite IHd, rev_rev; clear n m. } - unfold of_hexadecimal. - case d; intros i f; [|intro e]; unfold of_hexadecimal; simpl. - - case (Z.of_nat _)%Z; [|intro p..]; - [now exists (D1 Nil), O; split; [|left] - | |now exists (D1 Nil), O; split; [|left]]. - exists (D1 Nil), (Pos.to_nat p). - split; [|now left]; simpl. - change (Pos.iter _ _ _) with (Pos.iter (Pos.mul 2) 1%positive (4 * p)). - rewrite H. - rewrite Pos2Nat.inj_mul, Nat.mul_comm, Nat.div_mul; [|now simpl]. - now rewrite Nat.mod_mul; [|now simpl]. - - case (_ - _)%Z; [|intros p..]; [now exists (D1 Nil), O; split; [|left]..|]. - simpl Qden; rewrite H. - eexists; eexists; split; [reflexivity|]. - case (_ mod _); [now left|intro n]. - case n; [now right; left|clear n; intro n]. - case n; [now right; right; left|clear n; intro n]. - now right; right; right. } - generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint (Qden (of_hexadecimal d))). - destruct H as (h, (e, (He, Hh))); rewrite He; clear He. - assert (Hn1 : forall p, N.pos (Pos.iter (Pos.mul 2) 1%positive p) = 1%N -> False). - { intro p. - rewrite Pos2Nat.inj_iter. - case_eq (Pos.to_nat p); [|now simpl]. - intro H; exfalso; apply (lt_irrefl O). - rewrite <-H at 2; apply Pos2Nat.is_pos. } - assert (H16_2 : forall p, (16^p = 2^(4 * p))%positive). - { intro p. - apply (@f_equal _ _ (fun z => match z with Z.pos p => p | _ => 1%positive end) - (Z.pos _) (Z.pos _)). - rewrite !Pos2Z.inj_pow_pos, !Z.pow_pos_fold, Pos2Z.inj_mul. - now change 16%Z with (2^4)%Z; rewrite <-Z.pow_mul_r. } - assert (HN16_2 : forall n, (16^n = 2^(4 * n))%N). - { intro n. - apply N2Z.inj; rewrite !N2Z.inj_pow, N2Z.inj_mul. - change (Z.of_N 16) with (2^4)%Z. - now rewrite <-Z.pow_mul_r; [| |apply N2Z.is_nonneg]. } - assert (Hn1' : forall p, N.pos (Pos.iter (Pos.mul 16) 1%positive p) = 1%N -> False). - { intro p; fold (16^p)%positive; rewrite H16_2; apply Hn1. } - assert (Ht10inj : forall n m, t10 n = t10 m -> n = m). - { intros n m H; generalize (f_equal Z.pos H); clear H. - change (Z.pos (t10 n)) with (Z.mul 0x10 (Z.pos n)). - change (Z.pos (t10 m)) with (Z.mul 0x10 (Z.pos m)). - rewrite Z.mul_comm, (Z.mul_comm 0x10). - intro H; generalize (f_equal (fun z => Z.div z 0x10) H); clear H. - now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. } - assert (Ht2inj : forall n m, Pos.mul 2 n = Pos.mul 2 m -> n = m). - { intros n m H; generalize (f_equal Z.pos H); clear H. - change (Z.pos (Pos.mul 2 n)) with (Z.mul 2 (Z.pos n)). - change (Z.pos (Pos.mul 2 m)) with (Z.mul 2 (Z.pos m)). - rewrite Z.mul_comm, (Z.mul_comm 2). - intro H; generalize (f_equal (fun z => Z.div z 2) H); clear H. - now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. } - assert (Hinj : forall n m, - Nat.iter n (Pos.mul 2) 1%positive = Nat.iter m (Pos.mul 2) 1%positive - -> n = m). - { induction n; [now intro m; case m|]. - intro m; case m; [now simpl|]; clear m; intro m. - rewrite !Unsigned.nat_iter_S. - intro H; generalize (Ht2inj _ _ H); clear H; intro H. - now rewrite (IHn _ H). } - change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul. - change 1%Z with (Z.of_nat 1); rewrite <-Nat2Z.inj_add. - change 2%Z with (Z.of_nat 2); rewrite <-Nat2Z.inj_add. - change 3%Z with (Z.of_nat 3); rewrite <-Nat2Z.inj_add. - destruct Hh as [Hh|[Hh|[Hh|Hh]]]; rewrite Hh; clear h Hh. - - case e; clear e; [|intro e]; simpl; unfold of_hexadecimal, hnorme. - + case d; clear d; intros i f; [|intro e]. - * generalize (nb_digits_pos f). - case f; - [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2; - case nb_digits; - [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..]. - now intros _ _; simpl; rewrite to_of. - * rewrite <-DecimalZ.to_of, DecimalZ.of_to. - set (emf := (_ - _)%Z). - case_eq emf; [|intro pemf..]. - ++ now simpl; rewrite to_of. - ++ intros Hemf _; simpl. - apply f_equal, f_equal2; [|reflexivity]. - rewrite !Pos2Nat.inj_iter. - fold (Nat.iter (Pos.to_nat pemf) (Z.mul 2) (Z.of_hex_int (app_int i f))). - fold (Nat.iter (Pos.to_nat pemf) double (norm (app_int i f))). - induction Pos.to_nat; [now simpl; rewrite HexadecimalZ.to_of|]. - now rewrite !Unsigned.nat_iter_S, <-IHn, double_to_hex_int. - ++ simpl Qden; intros _ H; exfalso; revert H; apply Hn1. - + case d; clear d; intros i f; [|intro e']. - * simpl; case_eq (nb_digits f); [|intros nf' Hnf']; - [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1'|]. - unfold Z.of_nat, Z.opp, Qnum, Qden. - rewrite H16_2. - fold (Pos.mul 2); fold (2^(Pos.of_succ_nat nf')~0~0)%positive. - intro H; injection H; clear H. - unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H; intro H; injection H. - clear H; intro H; generalize (SuccNat2Pos.inj _ _ H); clear H. - intros <-. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite SuccNat2Pos.id_succ. - change (_~0)%positive with (4 * Pos.of_succ_nat nf')%positive. - now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ. - * set (nemf := (_ - _)%Z); intro H. - assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H]. - { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf]; - simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1'. } - destruct H' as (pnemf,Hpnemf); rewrite Hpnemf. - unfold Qnum, Qden. - rewrite H16_2. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H. - intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite SuccNat2Pos.id_succ. - change (_~0)%positive with (4 * Pos.of_succ_nat e)%positive. - now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ. - - simpl Pos.of_hex_uint. - rewrite HN16_2. - rewrite <-N.pow_succ_r; [|now apply N.le_0_l]. - rewrite <-N.succ_pos_spec. - case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme. - + set (em4f := (_ - _)%Z). - case_eq em4f; [|intros pem4f..]; intro Hpem4f; - [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. - unfold Qnum, Qden. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H; intros ->. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite SuccNat2Pos.id_succ. - case e; [now simpl|intro e'']; simpl. - unfold Pos.to_nat; simpl. - now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. - + set (em4f := (_ - _)%Z). - case_eq em4f; [|intros pem4f..]; intro Hpem4f; - [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. - unfold Qnum, Qden. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H; intros ->. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite SuccNat2Pos.id_succ. - case e; [now simpl|intro e'']; simpl. - unfold Pos.to_nat; simpl. - now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. - - simpl Pos.of_hex_uint. - rewrite HN16_2. - change 4%N with (2 * 2)%N at 1; rewrite <-!N.mul_assoc. - do 2 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]). - rewrite <-N.succ_pos_spec. - case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme. - + set (em4f := (_ - _)%Z). - case_eq em4f; [|intros pem4f..]; intro Hpem4f; - [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. - unfold Qnum, Qden. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H; intros ->. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite <-SuccNat2Pos.inj_succ. - rewrite SuccNat2Pos.id_succ. - case e; [now simpl|intro e'']; simpl. - unfold Pos.to_nat; simpl. - now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. - + set (em4f := (_ - _)%Z). - case_eq em4f; [|intros pem4f..]; intro Hpem4f; - [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. - unfold Qnum, Qden. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H; intros ->. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite <-SuccNat2Pos.inj_succ. - rewrite SuccNat2Pos.id_succ. - case e; [now simpl|intro e'']; simpl. - unfold Pos.to_nat; simpl. - now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. - - simpl Pos.of_hex_uint. - rewrite HN16_2. - change 8%N with (2 * 2 * 2)%N; rewrite <-!N.mul_assoc. - do 3 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]). - rewrite <-N.succ_pos_spec. - case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme. - + set (em4f := (_ - _)%Z). - case_eq em4f; [|intros pem4f..]; intro Hpem4f; - [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. - unfold Qnum, Qden. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H; intros ->. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite <-!SuccNat2Pos.inj_succ. - rewrite SuccNat2Pos.id_succ. - case e; [now simpl|intro e'']; simpl. - unfold Pos.to_nat; simpl. - now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. - + set (em4f := (_ - _)%Z). - case_eq em4f; [|intros pem4f..]; intro Hpem4f; - [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. - unfold Qnum, Qden. - intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. - intro H; generalize (Hinj _ _ H); clear H; intro H. - generalize (Pos2Nat.inj _ _ H); clear H; intros ->. - rewrite to_of. - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. - do 4 apply f_equal. - apply Pos2Nat.inj. - rewrite <-!SuccNat2Pos.inj_succ. - rewrite SuccNat2Pos.id_succ. - case e; [now simpl|intro e'']; simpl. - unfold Pos.to_nat; simpl. - now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. + case d as [i f|i f e]; case i as [i|i]. + - now simpl; rewrite unorm_involutive. + - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. + set (m := match nzhead _ with Nil =>_ | _ => _ end). + replace m with (Neg (unorm i)). + 2:{ now unfold m; revert Ha; case nzhead. } + case (uint_eq_dec (nzhead i) Nil); intro Hi. + + unfold unorm; rewrite Hi; simpl. + case (uint_eq_dec (nzhead f) Nil). + * intro Hf; exfalso; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + * now case nzhead. + + rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. + now revert Ha; case nzhead. + - simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He. + + now rewrite He; simpl; rewrite unorm_involutive. + + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). + replace m with (HexadecimalExp (Pos (unorm i)) f (Decimal.norm e)). + 2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. } + simpl; rewrite DecimalFacts.norm_involutive, unorm_involutive. + revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. + - simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He. + + rewrite He; simpl. + case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. + set (m := match nzhead _ with Nil =>_ | _ => _ end). + replace m with (Neg (unorm i)). + 2:{ now unfold m; revert Ha; case nzhead. } + case (uint_eq_dec (nzhead i) Nil); intro Hi. + * unfold unorm; rewrite Hi; simpl. + case (uint_eq_dec (nzhead f) Nil). + -- intro Hf; exfalso; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + -- now case nzhead. + * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. + now revert Ha; case nzhead. + + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). + pose (i' := match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end). + replace m with (HexadecimalExp i' f (Decimal.norm e)). + 2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. } + simpl; rewrite DecimalFacts.norm_involutive. + set (i'' := match i' with Pos _ => _ | _ => _ end). + clear m; set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). + replace m with (HexadecimalExp i'' f (Decimal.norm e)). + 2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. + now case e; clear e; [|intro e; case e|..]. } + unfold i'', i'. + case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. + fold i'; replace i' with (Neg (unorm i)). + 2:{ now unfold i'; revert Ha; case nzhead. } + case (uint_eq_dec (nzhead i) Nil); intro Hi. + * unfold unorm; rewrite Hi; simpl. + case (uint_eq_dec (nzhead f) Nil). + -- intro Hf; exfalso; apply Ha. + now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. + -- now case nzhead. + * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. + now revert Ha; case nzhead. +Qed. + +Lemma IZ_to_Z_IZ_of_Z z : IZ_to_Z (IZ_of_Z z) = Some z. +Proof. now case z. Qed. + +Lemma dnorm_i_exact i f : + (nb_digits f < nb_digits (unorm (app (abs i) f)))%nat -> + match i with + | Pos i => Pos (unorm i) + | Neg i => + match nzhead (app i f) with + | Nil => Pos zero + | _ => Neg (unorm i) + end + end = norm i. +Proof. + case i as [ni|ni]; [now simpl|]; simpl. + case (uint_eq_dec (nzhead (app ni f)) Nil); intro Ha. + { now rewrite Ha, (nzhead_app_nil_l _ _ Ha). } + rewrite (unorm_nzhead _ Ha). + set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (Neg (unorm ni)); [|now unfold m; revert Ha; case nzhead]. + case (uint_eq_dec (nzhead ni) Nil); intro Hni. + { rewrite <-nzhead_app_nzhead, Hni, app_nil_l. + intro H; exfalso; revert H; apply le_not_lt, nb_digits_nzhead. } + clear m; set (m := match nzhead ni with Nil => _ | _ => _ end). + replace m with (Neg (nzhead ni)); [|now unfold m; revert Hni; case nzhead]. + now rewrite (unorm_nzhead _ Hni). +Qed. + +Lemma dnorm_i_exact' i f : + (nb_digits (unorm (app (abs i) f)) <= nb_digits f)%nat -> + match i with + | Pos i => Pos (unorm i) + | Neg i => + match nzhead (app i f) with + | Nil => Pos zero + | _ => Neg (unorm i) + end + end = + match norm (app_int i f) with + | Pos _ => Pos zero + | Neg _ => Neg zero + end. +Proof. + case i as [ni|ni]; simpl. + { now intro Hnb; rewrite (unorm_app_zero _ _ Hnb). } + unfold unorm. + case (uint_eq_dec (nzhead (app ni f)) Nil); intro Hn. + { now rewrite Hn. } + set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (nzhead (app ni f)). + 2:{ now unfold m; revert Hn; case nzhead. } + clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (Neg (unorm ni)). + 2:{ now unfold m, unorm; revert Hn; case nzhead. } + clear m; set (m := match nzhead _ with Nil => _ | _ => _ end). + replace m with (Neg (nzhead (app ni f))). + 2:{ now unfold m; revert Hn; case nzhead. } + rewrite <-(unorm_nzhead _ Hn). + now intro H; rewrite (unorm_app_zero _ _ H). +Qed. + +Lemma to_of (d:hexadecimal) : to_hexadecimal (of_hexadecimal d) = Some (dnorm d). +Proof. + case d as [i f|i f e]. + - unfold of_hexadecimal; simpl; unfold IQmake_to_hexadecimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_hexadecimal; simpl. + change (fun _ : positive => _) with (Pos.mul 16). + rewrite nztail_to_hex_uint_pow16, to_of. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + + rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + + rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + * rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + * rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. + - unfold of_hexadecimal; simpl. + rewrite <-DecimalZ.to_of. + case (Z.of_int e); clear e; [|intro e..]; simpl. + + unfold IQmake_to_hexadecimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_hexadecimal; simpl. + change (fun _ : positive => _) with (Pos.mul 16). + rewrite nztail_to_hex_uint_pow16, to_of. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + * rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + -- rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + -- rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. + + unfold IQmake_to_hexadecimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_hexadecimal; simpl. + change (fun _ : positive => _) with (Pos.mul 16). + rewrite nztail_to_hex_uint_pow16, to_of. + generalize (DecimalPos.Unsigned.to_uint_nonzero e); intro He. + set (dnorm_i := match i with Pos _ => _ | _ => _ end). + set (m := match Pos.to_uint e with Decimal.Nil => _ | _ => _ end). + replace m with (HexadecimalExp dnorm_i f (Decimal.Pos (Pos.to_uint e))). + 2:{ now unfold m; revert He; case (Pos.to_uint e); [|intro u; case u|..]. } + clear m; unfold dnorm_i. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + * rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + -- rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + -- rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. + + unfold IQmake_to_hexadecimal'. + rewrite IZ_to_Z_IZ_of_Z. + unfold IQmake_to_hexadecimal; simpl. + change (fun _ : positive => _) with (Pos.mul 16). + rewrite nztail_to_hex_uint_pow16, to_of. + case_eq (nb_digits f); [|intro nb]; intro Hnb. + * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. + case i as [ni|ni]; [now simpl|]. + rewrite app_nil_r; simpl; unfold unorm. + now case (nzhead ni). + * rewrite <-Hnb. + rewrite abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnb'. + -- rewrite (del_tail_app_int_exact _ _ Hnb'). + rewrite (del_head_app_int_exact _ _ Hnb'). + now rewrite (dnorm_i_exact _ _ Hnb'). + -- rewrite (unorm_app_r _ _ Hnb'). + rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. + now rewrite dnorm_i_exact'. Qed. (** Some consequences *) @@ -466,68 +436,24 @@ Proof. now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). Qed. -Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (hnorme d). +Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (dnorm d). Proof. exists (of_hexadecimal d). apply to_of. Qed. -Lemma of_hexadecimal_hnorme d : of_hexadecimal (hnorme d) = of_hexadecimal d. -Proof. - unfold of_hexadecimal, hnorme. - destruct d. - - simpl Z.of_int; unfold Z.of_uint, Z.of_N, Pos.of_uint. - rewrite Z.sub_0_l. - set (n4f := (- _)%Z). - case_eq n4f; [|intro pn4f..]; intro Hn4f. - + apply f_equal2; [|reflexivity]. - rewrite app_int_nil_r. - now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. - + apply f_equal2; [|reflexivity]. - rewrite app_int_nil_r. - generalize (app_int i f); intro i'. - rewrite !Pos2Nat.inj_iter. - generalize (Pos.to_nat pn4f); intro n. - fold (Nat.iter n double (norm i')). - fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')). - induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|]. - now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double. - + unfold nb_digits, Z.of_nat. - rewrite Z.mul_0_r, Z.sub_0_r. - rewrite <-DecimalZ.to_of, !DecimalZ.of_to. - rewrite app_int_nil_r. - now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. - - set (nem4f := (_ - _)%Z). - case_eq nem4f; [|intro pnem4f..]; intro Hnem4f. - + apply f_equal2; [|reflexivity]. - rewrite app_int_nil_r. - now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. - + apply f_equal2; [|reflexivity]. - rewrite app_int_nil_r. - generalize (app_int i f); intro i'. - rewrite !Pos2Nat.inj_iter. - generalize (Pos.to_nat pnem4f); intro n. - fold (Nat.iter n double (norm i')). - fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')). - induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|]. - now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double. - + unfold nb_digits, Z.of_nat. - rewrite Z.mul_0_r, Z.sub_0_r. - rewrite <-DecimalZ.to_of, !DecimalZ.of_to. - rewrite app_int_nil_r. - now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. -Qed. +Lemma of_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d. +Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed. -Lemma of_inj d d' : - of_hexadecimal d = of_hexadecimal d' -> hnorme d = hnorme d'. +Lemma of_inj d d' : of_hexadecimal d = of_hexadecimal d' -> dnorm d = dnorm d'. Proof. - intros. - cut (Some (hnorme d) = Some (hnorme d')); [now intro H'; injection H'|]. - rewrite <- !to_of. now f_equal. + intro H. + apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end) + (Some (dnorm d)) (Some (dnorm d'))). + now rewrite <- !to_of, H. Qed. -Lemma of_iff d d' : - of_hexadecimal d = of_hexadecimal d' <-> hnorme d = hnorme d'. +Lemma of_iff d d' : of_hexadecimal d = of_hexadecimal d' <-> dnorm d = dnorm d'. Proof. - split. apply of_inj. intros E. rewrite <- of_hexadecimal_hnorme, E. - apply of_hexadecimal_hnorme. + split. apply of_inj. intros E. rewrite <- of_hexadecimal_dnorm, E. + apply of_hexadecimal_dnorm. Qed. diff --git a/theories/Numbers/HexadecimalR.v b/theories/Numbers/HexadecimalR.v new file mode 100644 index 0000000000..2deecc5847 --- /dev/null +++ b/theories/Numbers/HexadecimalR.v @@ -0,0 +1,302 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * HexadecimalR + + Proofs that conversions between hexadecimal numbers and [R] + are bijections. *) + +Require Import Decimal DecimalFacts. +Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ. +Require Import HexadecimalQ Rdefinitions. + +Lemma of_IQmake_to_hexadecimal num den : + match IQmake_to_hexadecimal num den with + | None => True + | Some (HexadecimalExp _ _ _) => False + | Some (Hexadecimal i f) => + of_hexadecimal (Hexadecimal i f) = IRQ (QArith_base.Qmake num den) + end. +Proof. + unfold IQmake_to_hexadecimal. + case (Pos.eq_dec den 1); [now intros->|intro Hden]. + assert (Hf : match QArith_base.IQmake_to_hexadecimal num den with + | Some (Hexadecimal i f) => f <> Nil + | _ => True + end). + { unfold QArith_base.IQmake_to_hexadecimal; simpl. + generalize (Unsigned.nztail_to_hex_uint den). + case Hexadecimal.nztail as [den' e_den']. + case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'. + case den'; [ |now simpl..]; clear den'. + case e_den' as [|e_den']; [now simpl; intros H _; apply Hden; injection H|]. + intros _. + case Nat.ltb_spec; intro He_den'. + - apply del_head_nonnil. + revert He_den'; case nb_digits as [|n]; [now simpl|]. + now intro H; simpl; apply le_lt_n_Sm, Nat.le_sub_l. + - apply nb_digits_n0. + now rewrite nb_digits_iter_D0, Nat.sub_add. } + replace (match den with 1%positive => _ | _ => _ end) + with (QArith_base.IQmake_to_hexadecimal num den); [|now revert Hden; case den]. + generalize (of_IQmake_to_hexadecimal num den). + case QArith_base.IQmake_to_hexadecimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + unfold of_hexadecimal; simpl. + intro H; injection H; clear H; intros <-. + intro H; generalize (f_equal QArith_base.IZ_to_Z H); clear H. + rewrite !IZ_to_Z_IZ_of_Z; intro H; injection H; clear H; intros<-. + now revert Hf; case f. +Qed. + +Lemma of_to (q:IR) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. +Proof. + intro d. + case q as [z|q|r r'|r r']; simpl. + - case z as [z p| |p|p]. + + now simpl. + + now simpl; intro H; injection H; clear H; intros<-. + + simpl; intro H; injection H; clear H; intros<-. + now unfold of_hexadecimal; simpl; unfold Z.of_hex_uint; rewrite Unsigned.of_to. + + simpl; intro H; injection H; clear H; intros<-. + now unfold of_hexadecimal; simpl; unfold Z.of_hex_uint; rewrite Unsigned.of_to. + - case q as [num den]. + generalize (of_IQmake_to_hexadecimal num den). + case IQmake_to_hexadecimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + now intros H H'; injection H'; intros<-. + - case r as [z|q| |]; [|case q as[num den]|now simpl..]; + (case r' as [z'| | |]; [|now simpl..]); + (case z' as [p e| | |]; [|now simpl..]). + + case (Z.eq_dec p 2); [intros->|intro Hp]. + 2:{ now revert Hp; case p; + [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } + case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-. + * now unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. + * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + now unfold Z.of_hex_uint; rewrite Unsigned.of_to. + * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + now unfold Z.of_hex_uint; rewrite Unsigned.of_to. + + case (Z.eq_dec p 2); [intros->|intro Hp]. + 2:{ now revert Hp; case p; + [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } + generalize (of_IQmake_to_hexadecimal num den). + case IQmake_to_hexadecimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros H H'; injection H'; clear H'; intros<-. + unfold of_hexadecimal; simpl. + change (match f with Nil => _ | _ => _ end) with (of_hexadecimal (Hexadecimal i f)). + rewrite H; clear H. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. + - case r as [z|q| |]; [|case q as[num den]|now simpl..]; + (case r' as [z'| | |]; [|now simpl..]); + (case z' as [p e| | |]; [|now simpl..]). + + case (Z.eq_dec p 2); [intros->|intro Hp]. + 2:{ now revert Hp; case p; + [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } + case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-. + * now unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. + * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + now unfold Z.of_hex_uint; rewrite Unsigned.of_to. + * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + now unfold Z.of_hex_uint; rewrite Unsigned.of_to. + + case (Z.eq_dec p 2); [intros->|intro Hp]. + 2:{ now revert Hp; case p; + [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } + generalize (of_IQmake_to_hexadecimal num den). + case IQmake_to_hexadecimal as [d'|]; [|now simpl]. + case d' as [i f|]; [|now simpl]. + intros H H'; injection H'; clear H'; intros<-. + unfold of_hexadecimal; simpl. + change (match f with Nil => _ | _ => _ end) with (of_hexadecimal (Hexadecimal i f)). + rewrite H; clear H. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. +Qed. + +Lemma to_of (d:hexadecimal) : to_hexadecimal (of_hexadecimal d) = Some (dnorm d). +Proof. + case d as [i f|i f e]. + - unfold of_hexadecimal; simpl. + case (uint_eq_dec f Nil); intro Hf. + + rewrite Hf; clear f Hf. + unfold to_hexadecimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + + set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_hexadecimal; simpl. + unfold IQmake_to_hexadecimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_hexadecimal, n; simpl. + rewrite nztail_to_hex_uint_pow16. + clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite HexadecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + * rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + * rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. + - unfold of_hexadecimal; simpl. + rewrite <-(DecimalZ.to_of e). + case (Z.of_int e); clear e; [|intro e..]; simpl. + + case (uint_eq_dec f Nil); intro Hf. + * rewrite Hf; clear f Hf. + unfold to_hexadecimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + * set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_hexadecimal; simpl. + unfold IQmake_to_hexadecimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_hexadecimal, n; simpl. + rewrite nztail_to_hex_uint_pow16. + clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite HexadecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + -- rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + -- rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. + + set (i' := match i with Pos _ => _ | _ => _ end). + set (m := match Pos.to_uint e with Decimal.Nil => _ | _ => _ end). + replace m with (HexadecimalExp i' f (Decimal.Pos (Pos.to_uint e))). + 2:{ unfold m; generalize (DecimalPos.Unsigned.to_uint_nonzero e). + now case Pos.to_uint; [|intro u; case u|..]. } + unfold i'; clear i' m. + case (uint_eq_dec f Nil); intro Hf. + * rewrite Hf; clear f Hf. + unfold to_hexadecimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + * set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_hexadecimal; simpl. + unfold IQmake_to_hexadecimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_hexadecimal, n; simpl. + rewrite nztail_to_hex_uint_pow16. + clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite HexadecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + -- rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + -- rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. + + case (uint_eq_dec f Nil); intro Hf. + * rewrite Hf; clear f Hf. + unfold to_hexadecimal; simpl. + rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of. + case i as [i|i]; [now simpl|]; simpl. + rewrite app_nil_r. + case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. + now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + * set (r := IRQ _). + set (m := match f with Nil => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + unfold to_hexadecimal; simpl. + unfold IQmake_to_hexadecimal; simpl. + set (n := Nat.iter _ _ _). + case (Pos.eq_dec n 1); intro Hn. + exfalso; apply Hf. + { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } + clear m; set (m := match n with 1%positive | _ => _ end). + replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n). + 2:{ now unfold m; revert Hn; case n. } + unfold QArith_base.IQmake_to_hexadecimal, n; simpl. + rewrite nztail_to_hex_uint_pow16. + clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _). + clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). + replace m with r; [unfold r|now unfold m; revert Hf; case f]. + rewrite HexadecimalZ.to_of, abs_norm, abs_app_int. + case Nat.ltb_spec; intro Hnf. + -- rewrite (del_tail_app_int_exact _ _ Hnf). + rewrite (del_head_app_int_exact _ _ Hnf). + now rewrite (dnorm_i_exact _ _ Hnf). + -- rewrite (unorm_app_r _ _ Hnf). + rewrite (iter_D0_unorm _ Hf). + now rewrite dnorm_i_exact'. +Qed. + +(** Some consequences *) + +Lemma to_hexadecimal_inj q q' : + to_hexadecimal q <> None -> to_hexadecimal q = to_hexadecimal q' -> q = q'. +Proof. + intros Hnone EQ. + generalize (of_to q) (of_to q'). + rewrite <-EQ. + revert Hnone; case to_hexadecimal; [|now simpl]. + now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). +Qed. + +Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (dnorm d). +Proof. + exists (of_hexadecimal d). apply to_of. +Qed. + +Lemma of_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d. +Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed. + +Lemma of_inj d d' : of_hexadecimal d = of_hexadecimal d' -> dnorm d = dnorm d'. +Proof. + intro H. + apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end) + (Some (dnorm d)) (Some (dnorm d'))). + now rewrite <- !to_of, H. +Qed. + +Lemma of_iff d d' : of_hexadecimal d = of_hexadecimal d' <-> dnorm d = dnorm d'. +Proof. + split. apply of_inj. intros E. rewrite <- of_hexadecimal_dnorm, E. + apply of_hexadecimal_dnorm. +Qed. diff --git a/theories/Numbers/HexadecimalZ.v b/theories/Numbers/HexadecimalZ.v index c5ed0b5b28..1d78ad1ad2 100644 --- a/theories/Numbers/HexadecimalZ.v +++ b/theories/Numbers/HexadecimalZ.v @@ -80,9 +80,11 @@ Lemma of_hex_uint_iter_D0 d n : Z.of_hex_uint (app d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 0x10) (Z.of_hex_uint d). Proof. - unfold Z.of_hex_uint. - unfold app; rewrite <-rev_revapp. - rewrite Unsigned.of_lu_rev, Unsigned.of_lu_revapp. + rewrite <-(rev_rev (app _ _)), <-(of_list_to_list (rev (app _ _))). + rewrite rev_spec, app_spec, List.rev_app_distr. + rewrite <-!rev_spec, <-app_spec, of_list_to_list. + unfold Z.of_hex_uint; rewrite Unsigned.of_lu_rev. + unfold app; rewrite Unsigned.of_lu_revapp, !rev_rev. rewrite <-!Unsigned.of_lu_rev, !rev_rev. assert (H' : Pos.of_hex_uint (Nat.iter n D0 Nil) = 0%N). { now induction n; [|rewrite Unsigned.nat_iter_S]. } @@ -140,3 +142,22 @@ Qed. Lemma double_to_hex_int n : double (Z.to_hex_int n) = Z.to_hex_int (Z.double n). Proof. now rewrite <-(of_to n), <-of_hex_int_double, !to_of, double_norm. Qed. + +Lemma nztail_to_hex_uint_pow16 n : + Hexadecimal.nztail (Pos.to_hex_uint (Nat.iter n (Pos.mul 16) 1%positive)) + = (D1 Nil, n). +Proof. + case n as [|n]; [now simpl|]. + rewrite <-(Nat2Pos.id (S n)); [|now simpl]. + generalize (Pos.of_nat (S n)); clear n; intro p. + induction (Pos.to_nat p); [now simpl|]. + rewrite Unsigned.nat_iter_S. + unfold Pos.to_hex_uint. + change (Pos.to_little_hex_uint _) + with (Unsigned.to_lu (16 * N.pos (Nat.iter n (Pos.mul 16) 1%positive))). + rewrite Unsigned.to_lhex_tenfold. + revert IHn; unfold Pos.to_hex_uint. + unfold Hexadecimal.nztail; rewrite !rev_rev; simpl. + set (f'' := _ (Pos.to_little_hex_uint _)). + now case f''; intros r n' H; inversion H. +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. |