diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/DoubleType.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 35 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Ring31.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Cyclic63.v | 330 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 1918 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Ring63.v | 65 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 25 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAddOrder.v | 22 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 190 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZGcd.v | 104 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZLog.v | 601 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 25 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMulOrder.v | 191 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 175 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZParity.v | 64 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 326 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 493 |
19 files changed, 3458 insertions, 1131 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index b6441bb76a..9547a642df 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -12,7 +12,7 @@ Set Implicit Arguments. -Require Import ZArith. +Require Import BinInt. Local Open Scope Z_scope. Definition base digits := Z.pow 2 (Zpos digits). @@ -23,7 +23,7 @@ Section Carry. Variable A : Type. #[universes(template)] - Inductive carry := + Variant carry := | C0 : A -> carry | C1 : A -> carry. @@ -46,7 +46,7 @@ Section Zn2Z. *) #[universes(template)] - Inductive zn2z := + Variant zn2z := | W0 : zn2z | WW : znz -> znz -> zn2z. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 4a1f24b95e..4b0bda3d44 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** This library has been deprecated since Coq version 8.10. *) + (** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *) (** @@ -1274,7 +1276,7 @@ Section Int31_Specs. Qed. Lemma spec_add_carry : - forall x y, [|x+y+1|] = ([|x|] + [|y|] + 1) mod wB. + forall x y, [|x+y+1|] = ([|x|] + [|y|] + 1) mod wB. Proof. unfold add31; intros. repeat rewrite phi_phi_inv. @@ -1776,7 +1778,7 @@ Section Int31_Specs. Qed. Lemma spec_head0 : forall x, 0 < [|x|] -> - wB/ 2 <= 2 ^ ([|head031 x|]) * [|x|] < wB. + wB/ 2 <= 2 ^ ([|head031 x|]) * [|x|] < wB. Proof. intros. rewrite head031_equiv. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index ce540775e3..b9185c9ca0 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -10,6 +10,8 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) +(** This library has been deprecated since Coq version 8.10. *) + Require Import NaryFunctions. Require Import Wf_nat. Require Export ZArith. @@ -44,18 +46,11 @@ Definition digits31 t := Eval compute in nfun digits size t. Inductive int31 : Type := I31 : digits31 int31. -(* spiwack: Registration of the type of integers, so that the matchs in - the functions below perform dynamic decompilation (otherwise some segfault - occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31.bits. -Register int31 as int31.type. - Scheme int31_ind := Induction for int31 Sort Prop. Scheme int31_rec := Induction for int31 Sort Set. Scheme int31_rect := Induction for int31 Sort Type. Declare Scope int31_scope. -Declare ML Module "int31_syntax_plugin". Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. @@ -208,6 +203,13 @@ Definition phi_inv : Z -> int31 := fun n => | Zneg p => incr (complement_negative p) end. +(** [phi_inv_nonneg] returns [None] if the [Z] is negative; this matches the old behavior of parsing int31 numerals *) +Definition phi_inv_nonneg : Z -> option int31 := fun n => + match n with + | Zneg _ => None + | _ => Some (phi_inv n) + end. + (** [phi_inv2] is similar to [phi_inv] but returns a double word [zn2z int31] *) @@ -351,22 +353,6 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31.plus. -Register add31c as int31.plusc. -Register add31carryc as int31.pluscarryc. -Register sub31 as int31.minus. -Register sub31c as int31.minusc. -Register sub31carryc as int31.minuscarryc. -Register mul31 as int31.times. -Register mul31c as int31.timesc. -Register div3121 as int31.div21. -Register div31 as int31.diveucl. -Register compare31 as int31.compare. -Register addmuldiv31 as int31.addmuldiv. -Register lor31 as int31.lor. -Register land31 as int31.land. -Register lxor31 as int31.lxor. - Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -491,5 +477,4 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31.head0. -Register tail031 as int31.tail0. +Numeral Notation int31 phi_inv_nonneg phi : int31_scope. diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index b693529451..eb47141cab 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** This library has been deprecated since Coq version 8.10. *) + (** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped with a ring structure and a ring tactic *) @@ -101,4 +103,3 @@ Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x. intros. ring. Qed. End TestRing. - diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v new file mode 100644 index 0000000000..3b431d5b47 --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -0,0 +1,330 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Int63 numbers defines indeed a cyclic structure : Z/(2^31)Z *) + +(** +Author: Arnaud Spiwack (+ Pierre Letouzey) +*) +Require Import CyclicAxioms. +Require Export ZArith. +Require Export Int63. +Import Zpow_facts. +Import Utf8. +Import Lia. + +Local Open Scope int63_scope. +(** {2 Operators } **) + +Definition Pdigits := Eval compute in P_of_succ_nat (size - 1). + +Fixpoint positive_to_int_rec (n:nat) (p:positive) := + match n, p with + | O, _ => (Npos p, 0) + | S n, xH => (0%N, 1) + | S n, xO p => + let (N,i) := positive_to_int_rec n p in + (N, i << 1) + | S n, xI p => + let (N,i) := positive_to_int_rec n p in + (N, (i << 1) + 1) + end. + +Definition positive_to_int := positive_to_int_rec size. + +Definition mulc_WW x y := + let (h, l) := mulc x y in + if is_zero h then + if is_zero l then W0 + else WW h l + else WW h l. +Notation "n '*c' m" := (mulc_WW n m) (at level 40, no associativity) : int63_scope. + +Definition pos_mod p x := + if p <= digits then + let p := digits - p in + (x << p) >> p + else x. + +Notation pos_mod_int := pos_mod. + +Import ZnZ. + +Instance int_ops : ZnZ.Ops int := +{| + digits := Pdigits; (* number of digits *) + zdigits := Int63.digits; (* number of digits *) + to_Z := Int63.to_Z; (* conversion to Z *) + of_pos := positive_to_int; (* positive -> N*int63 : p => N,i + where p = N*2^31+phi i *) + head0 := Int63.head0; (* number of head 0 *) + tail0 := Int63.tail0; (* number of tail 0 *) + zero := 0; + one := 1; + minus_one := Int63.max_int; + compare := Int63.compare; + eq0 := Int63.is_zero; + opp_c := Int63.oppc; + opp := Int63.opp; + opp_carry := Int63.oppcarry; + succ_c := Int63.succc; + add_c := Int63.addc; + add_carry_c := Int63.addcarryc; + succ := Int63.succ; + add := Int63.add; + add_carry := Int63.addcarry; + pred_c := Int63.predc; + sub_c := Int63.subc; + sub_carry_c := Int63.subcarryc; + pred := Int63.pred; + sub := Int63.sub; + sub_carry := Int63.subcarry; + mul_c := mulc_WW; + mul := Int63.mul; + square_c := fun x => mulc_WW x x; + div21 := diveucl_21; + div_gt := diveucl; (* this is supposed to be the special case of + division a/b where a > b *) + div := diveucl; + modulo_gt := Int63.mod; + modulo := Int63.mod; + gcd_gt := Int63.gcd; + gcd := Int63.gcd; + add_mul_div := Int63.addmuldiv; + pos_mod := pos_mod_int; + is_even := Int63.is_even; + sqrt2 := Int63.sqrt2; + sqrt := Int63.sqrt; + ZnZ.lor := Int63.lor; + ZnZ.land := Int63.land; + ZnZ.lxor := Int63.lxor +|}. + +Local Open Scope Z_scope. + +Lemma is_zero_spec_aux : forall x : int, is_zero x = true -> [|x|] = 0%Z. +Proof. + intros x;rewrite is_zero_spec;intros H;rewrite H;trivial. +Qed. + +Lemma positive_to_int_spec : + forall p : positive, + Zpos p = + Z_of_N (fst (positive_to_int p)) * wB + to_Z (snd (positive_to_int p)). +Proof. + assert (H: (wB <= wB) -> forall p : positive, + Zpos p = Z_of_N (fst (positive_to_int p)) * wB + [|snd (positive_to_int p)|] /\ + [|snd (positive_to_int p)|] < wB). + 2: intros p; case (H (Z.le_refl wB) p); auto. + unfold positive_to_int, wB at 1 3 4. + elim size. + intros _ p; simpl; + rewrite to_Z_0, Pmult_1_r; split; auto with zarith; apply refl_equal. + intros n; rewrite inj_S; unfold Z.succ; rewrite Zpower_exp, Z.pow_1_r; auto with zarith. + intros IH Hle p. + assert (F1: 2 ^ Z_of_nat n <= wB); auto with zarith. + assert (0 <= 2 ^ Z_of_nat n); auto with zarith. + case p; simpl. + intros p1. + generalize (IH F1 p1); case positive_to_int_rec; simpl. + intros n1 i (H1,H2). + rewrite Zpos_xI, H1. + replace [|i << 1 + 1|] with ([|i|] * 2 + 1). + split; auto with zarith; ring. + rewrite add_spec, lsl_spec, Zplus_mod_idemp_l, to_Z_1, Z.pow_1_r, Zmod_small; auto. + case (to_Z_bounded i); split; auto with zarith. + intros p1. + generalize (IH F1 p1); case positive_to_int_rec; simpl. + intros n1 i (H1,H2). + rewrite Zpos_xO, H1. + replace [|i << 1|] with ([|i|] * 2). + split; auto with zarith; ring. + rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto. + case (to_Z_bounded i); split; auto with zarith. + rewrite to_Z_1; assert (0 < 2^ Z_of_nat n); auto with zarith. +Qed. + +Lemma mulc_WW_spec : + forall x y,[|| x *c y ||] = [|x|] * [|y|]. +Proof. + intros x y;unfold mulc_WW. + generalize (mulc_spec x y);destruct (mulc x y);simpl;intros Heq;rewrite Heq. + case_eq (is_zero i);intros;trivial. + apply is_zero_spec in H;rewrite H, to_Z_0. + case_eq (is_zero i0);intros;trivial. + apply is_zero_spec in H0;rewrite H0, to_Z_0, Zmult_comm;trivial. +Qed. + +Lemma squarec_spec : + forall x, + [||x *c x||] = [|x|] * [|x|]. +Proof (fun x => mulc_WW_spec x x). + +Lemma diveucl_spec_aux : forall a b, 0 < [|b|] -> + let (q,r) := diveucl a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. +Proof. + intros a b H;assert (W:= diveucl_spec a b). + assert ([|b|]>0) by (auto with zarith). + generalize (Z_div_mod [|a|] [|b|] H0). + destruct (diveucl a b);destruct (Z.div_eucl [|a|] [|b|]). + inversion W;rewrite Zmult_comm;trivial. +Qed. + +Lemma diveucl_21_spec_aux : forall a1 a2 b, + wB/2 <= [|b|] -> + [|a1|] < [|b|] -> + let (q,r) := diveucl_21 a1 a2 b in + [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]. +Proof. + intros a1 a2 b H1 H2;assert (W:= diveucl_21_spec a1 a2 b). + assert (W1:= to_Z_bounded a1). + assert ([|b|]>0) by (auto with zarith). + generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H). + destruct (diveucl_21 a1 a2 b);destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]). + inversion W;rewrite (Zmult_comm [|b|]);trivial. +Qed. + +Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n -> + ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) = + a mod 2 ^ p. + Proof. + intros n p a H. + rewrite Zmod_small. + - rewrite Zmod_eq by auto with zarith. + unfold Zminus at 1. + rewrite Zdiv.Z_div_plus_full_l by auto with zarith. + replace (2 ^ n) with (2 ^ (n - p) * 2 ^ p) by (rewrite <- Zpower_exp; [ f_equal | | ]; lia). + rewrite <- Zdiv_Zdiv, Z_div_mult by auto with zarith. + rewrite (Zmult_comm (2^(n-p))), Zmult_assoc. + rewrite Zopp_mult_distr_l. + rewrite Z_div_mult by auto with zarith. + symmetry; apply Zmod_eq; auto with zarith. + - remember (a * 2 ^ (n - p)) as b. + destruct (Z_mod_lt b (2^n)); auto with zarith. + split. + apply Z_div_pos; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + apply Z.lt_le_trans with (2^n); auto with zarith. + generalize (pow2_pos (n - p)); nia. + Qed. + +Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p. + Proof. + intros p x Hle;destruct (Z_le_gt_dec 0 p). + apply Zdiv_le_lower_bound;auto with zarith. + replace (2^p) with 0. + destruct x;compute;intro;discriminate. + destruct p;trivial;discriminate. + Qed. + +Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. + Proof. + intros p x y H;destruct (Z_le_gt_dec 0 p). + apply Zdiv_lt_upper_bound;auto with zarith. + apply Z.lt_le_trans with y;auto with zarith. + rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith. + assert (0 < 2^p);auto with zarith. + replace (2^p) with 0. + destruct x;change (0<y);auto with zarith. + destruct p;trivial;discriminate. + Qed. + +Lemma P (A B C: Prop) : + A → (B → C) → (A → B) → C. +Proof. tauto. Qed. + +Lemma shift_unshift_mod_3: + forall n p a : Z, + 0 <= p <= n -> + (a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) = a mod 2 ^ p. +Proof. + intros;rewrite <- (shift_unshift_mod_2 n p a);[ | auto with zarith]. + symmetry;apply Zmod_small. + generalize (a * 2 ^ (n - p));intros w. + generalize (2 ^ (n - p)) (pow2_pos (n - p)); intros x; apply P. lia. intros hx. + generalize (2 ^ n) (pow2_pos n); intros y; apply P. lia. intros hy. + elim_div. intros q r. apply P. lia. + elim_div. intros z t. refine (P _ _ _ _ _). lia. + intros [ ? [ ht | ] ]; [ | lia ]; subst w. + intros [ ? [ hr | ] ]; [ | lia ]; subst t. + nia. +Qed. + +Lemma pos_mod_spec w p : φ(pos_mod p w) = φ(w) mod (2 ^ φ(p)). +Proof. + simpl. unfold pos_mod_int. + assert (W:=to_Z_bounded p);assert (W':=to_Z_bounded Int63.digits);assert (W'' := to_Z_bounded w). + case lebP; intros hle. + 2: { + symmetry; apply Zmod_small. + assert (2 ^ [|Int63.digits|] < 2 ^ [|p|]); [ apply Zpower_lt_monotone; auto with zarith | ]. + change wB with (2 ^ [|Int63.digits|]) in *; auto with zarith. } + rewrite <- (shift_unshift_mod_3 [|Int63.digits|] [|p|] [|w|]) by auto with zarith. + replace ([|Int63.digits|] - [|p|]) with [|Int63.digits - p|] by (rewrite sub_spec, Zmod_small; auto with zarith). + rewrite lsr_spec, lsl_spec; reflexivity. +Qed. + +(** {2 Specification and proof} **) +Global Instance int_specs : ZnZ.Specs int_ops := { + spec_to_Z := to_Z_bounded; + spec_of_pos := positive_to_int_spec; + spec_zdigits := refl_equal _; + spec_more_than_1_digit:= refl_equal _; + spec_0 := to_Z_0; + spec_1 := to_Z_1; + spec_m1 := refl_equal _; + spec_compare := compare_spec; + spec_eq0 := is_zero_spec_aux; + spec_opp_c := oppc_spec; + spec_opp := opp_spec; + spec_opp_carry := oppcarry_spec; + spec_succ_c := succc_spec; + spec_add_c := addc_spec; + spec_add_carry_c := addcarryc_spec; + spec_succ := succ_spec; + spec_add := add_spec; + spec_add_carry := addcarry_spec; + spec_pred_c := predc_spec; + spec_sub_c := subc_spec; + spec_sub_carry_c := subcarryc_spec; + spec_pred := pred_spec; + spec_sub := sub_spec; + spec_sub_carry := subcarry_spec; + spec_mul_c := mulc_WW_spec; + spec_mul := mul_spec; + spec_square_c := squarec_spec; + spec_div21 := diveucl_21_spec_aux; + spec_div_gt := fun a b _ => diveucl_spec_aux a b; + spec_div := diveucl_spec_aux; + spec_modulo_gt := fun a b _ _ => mod_spec a b; + spec_modulo := fun a b _ => mod_spec a b; + spec_gcd_gt := fun a b _ => gcd_spec a b; + spec_gcd := gcd_spec; + spec_head00 := head00_spec; + spec_head0 := head0_spec; + spec_tail00 := tail00_spec; + spec_tail0 := tail0_spec; + spec_add_mul_div := addmuldiv_spec; + spec_pos_mod := pos_mod_spec; + spec_is_even := is_even_spec; + spec_sqrt2 := sqrt2_spec; + spec_sqrt := sqrt_spec; + spec_land := land_spec'; + spec_lor := lor_spec'; + spec_lxor := lxor_spec' }. + + + +Module Int63Cyclic <: CyclicType. + Definition t := int. + Definition ops := int_ops. + Definition specs := int_specs. +End Int63Cyclic. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v new file mode 100644 index 0000000000..eac26add03 --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -0,0 +1,1918 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +Require Import Utf8. +Require Export DoubleType. +Require Import Lia. +Require Import Zpow_facts. +Require Import Zgcd_alt. +Import Znumtheory. + +Register bool as kernel.ind_bool. +Register prod as kernel.ind_pair. +Register carry as kernel.ind_carry. +Register comparison as kernel.ind_cmp. + +Definition size := 63%nat. + +Primitive int := #int63_type. +Register int as num.int63.type. +Declare Scope int63_scope. +Definition id_int : int -> int := fun x => x. +Declare ML Module "int63_syntax_plugin". + +Delimit Scope int63_scope with int63. +Bind Scope int63_scope with int. + +(* Logical operations *) +Primitive lsl := #int63_lsl. +Infix "<<" := lsl (at level 30, no associativity) : int63_scope. + +Primitive lsr := #int63_lsr. +Infix ">>" := lsr (at level 30, no associativity) : int63_scope. + +Primitive land := #int63_land. +Infix "land" := land (at level 40, left associativity) : int63_scope. + +Primitive lor := #int63_lor. +Infix "lor" := lor (at level 40, left associativity) : int63_scope. + +Primitive lxor := #int63_lxor. +Infix "lxor" := lxor (at level 40, left associativity) : int63_scope. + +(* Arithmetic modulo operations *) +Primitive add := #int63_add. +Notation "n + m" := (add n m) : int63_scope. + +Primitive sub := #int63_sub. +Notation "n - m" := (sub n m) : int63_scope. + +Primitive mul := #int63_mul. +Notation "n * m" := (mul n m) : int63_scope. + +Primitive mulc := #int63_mulc. + +Primitive div := #int63_div. +Notation "n / m" := (div n m) : int63_scope. + +Primitive mod := #int63_mod. +Notation "n '\%' m" := (mod n m) (at level 40, left associativity) : int63_scope. + +(* Comparisons *) +Primitive eqb := #int63_eq. +Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + +Primitive ltb := #int63_lt. +Notation "m < n" := (ltb m n) : int63_scope. + +Primitive leb := #int63_le. +Notation "m <= n" := (leb m n) : int63_scope. +Notation "m ≤ n" := (leb m n) (at level 70, no associativity) : int63_scope. + +Local Open Scope int63_scope. + +(** The number of digits as a int *) +Definition digits := 63. + +(** The bigger int *) +Definition max_int := Eval vm_compute in 0 - 1. +Register Inline max_int. + +(** Access to the nth digits *) +Definition get_digit x p := (0 < (x land (1 << p))). + +Definition set_digit x p (b:bool) := + if if 0 <= p then p < digits else false then + if b then x lor (1 << p) + else x land (max_int lxor (1 << p)) + else x. + +(** Equality to 0 *) +Definition is_zero (i:int) := i == 0. +Register Inline is_zero. + +(** Parity *) +Definition is_even (i:int) := is_zero (i land 1). +Register Inline is_even. + +(** Bit *) + +Definition bit i n := negb (is_zero ((i >> n) << (digits - 1))). +(* Register bit as PrimInline. *) + +(** Extra modulo operations *) +Definition opp (i:int) := 0 - i. +Register Inline opp. +Notation "- x" := (opp x) : int63_scope. + +Definition oppcarry i := max_int - i. +Register Inline oppcarry. + +Definition succ i := i + 1. +Register Inline succ. + +Definition pred i := i - 1. +Register Inline pred. + +Definition addcarry i j := i + j + 1. +Register Inline addcarry. + +Definition subcarry i j := i - j - 1. +Register Inline subcarry. + +(** Exact arithmetic operations *) + +Definition addc_def x y := + let r := x + y in + if r < x then C1 r else C0 r. +(* the same but direct implementation for effeciancy *) +Primitive addc := #int63_addc. +Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. + +Definition addcarryc_def x y := + let r := addcarry x y in + if r <= x then C1 r else C0 r. +(* the same but direct implementation for effeciancy *) +Primitive addcarryc := #int63_addcarryc. + +Definition subc_def x y := + if y <= x then C0 (x - y) else C1 (x - y). +(* the same but direct implementation for effeciancy *) +Primitive subc := #int63_subc. +Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. + +Definition subcarryc_def x y := + if y < x then C0 (x - y - 1) else C1 (x - y - 1). +(* the same but direct implementation for effeciancy *) +Primitive subcarryc := #int63_subcarryc. + +Definition diveucl_def x y := (x/y, x\%y). +(* the same but direct implementation for effeciancy *) +Primitive diveucl := #int63_diveucl. + +Primitive diveucl_21 := #int63_div21. + +Definition addmuldiv_def p x y := + (x << p) lor (y >> (digits - p)). +Primitive addmuldiv := #int63_addmuldiv. + +Definition oppc (i:int) := 0 -c i. +Register Inline oppc. + +Definition succc i := i +c 1. +Register Inline succc. + +Definition predc i := i -c 1. +Register Inline predc. + +(** Comparison *) +Definition compare_def x y := + if x < y then Lt + else if (x == y) then Eq else Gt. + +Primitive compare := #int63_compare. +Notation "n ?= m" := (compare n m) (at level 70, no associativity) : int63_scope. + +Import Bool ZArith. +(** Translation to Z *) +Fixpoint to_Z_rec (n:nat) (i:int) := + match n with + | O => 0%Z + | S n => + (if is_even i then Z.double else Zdouble_plus_one) (to_Z_rec n (i >> 1)) + end. + +Definition to_Z := to_Z_rec size. + +Fixpoint of_pos_rec (n:nat) (p:positive) := + match n, p with + | O, _ => 0 + | S n, xH => 1 + | S n, xO p => (of_pos_rec n p) << 1 + | S n, xI p => (of_pos_rec n p) << 1 lor 1 + end. + +Definition of_pos := of_pos_rec size. + +Definition of_Z z := + match z with + | Zpos p => of_pos p + | Z0 => 0 + | Zneg p => - (of_pos p) + end. + +Notation "[| x |]" := (to_Z x) (at level 0, x at level 99) : int63_scope. + +Definition wB := (2 ^ (Z.of_nat size))%Z. + +Lemma to_Z_rec_bounded size : forall x, (0 <= to_Z_rec size x < 2 ^ Z.of_nat size)%Z. +Proof. + elim size. simpl; auto with zarith. + intros n ih x; rewrite inj_S; simpl; assert (W := ih (x >> 1)%int63). + rewrite Z.pow_succ_r; auto with zarith. + destruct (is_even x). + rewrite Zdouble_mult; auto with zarith. + rewrite Zdouble_plus_one_mult; auto with zarith. +Qed. + +Corollary to_Z_bounded : forall x, (0 <= [| x |] < wB)%Z. +Proof. apply to_Z_rec_bounded. Qed. + +(* =================================================== *) +Local Open Scope Z_scope. +(* General arithmetic results *) +Lemma Z_lt_div2 x y : x < 2 * y -> x / 2 < y. +Proof. apply Z.div_lt_upper_bound; reflexivity. Qed. + +Theorem Zmod_le_first a b : 0 <= a -> 0 < b -> 0 <= a mod b <= a. +Proof. + intros ha hb; case (Z_mod_lt a b); [ auto with zarith | ]; intros p q; apply (conj p). + case (Z.le_gt_cases b a). lia. + intros hlt; rewrite Zmod_small; lia. +Qed. + +Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> + (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t. +Proof. + intros a b r t (H1, H2) H3 (H4, H5). + assert (t < 2 ^ b). + apply Z.lt_le_trans with (1:= H5); auto with zarith. + apply Zpower_le_monotone; auto with zarith. + rewrite Zplus_mod; auto with zarith. + rewrite -> Zmod_small with (a := t); auto with zarith. + apply Zmod_small; auto with zarith. + split; auto with zarith. + assert (0 <= 2 ^a * r); auto with zarith. + apply Z.add_nonneg_nonneg; auto with zarith. + match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; + auto with zarith. + pattern (2 ^ b) at 2; replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); + try ring. + apply Z.add_le_lt_mono; auto with zarith. + replace b with ((b - a) + a); try ring. + rewrite Zpower_exp; auto with zarith. + pattern (2 ^a) at 4; rewrite <- (Z.mul_1_l (2 ^a)); + try rewrite <- Z.mul_sub_distr_r. + rewrite (Z.mul_comm (2 ^(b - a))); rewrite Zmult_mod_distr_l; + auto with zarith. + rewrite (Z.mul_comm (2 ^a)); apply Z.mul_le_mono_nonneg_r; auto with zarith. + match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end. + apply Z.lt_gt; auto with zarith. + auto with zarith. +Qed. + +(* Results about pow2 *) +Lemma pow2_pos n : 0 <= n → 2 ^ n > 0. +Proof. intros h; apply Z.lt_gt, Zpower_gt_0; lia. Qed. + +Lemma pow2_nz n : 0 <= n → 2 ^ n ≠ 0. +Proof. intros h; generalize (pow2_pos _ h); lia. Qed. + +Hint Resolve pow2_pos pow2_nz : zarith. + +(* =================================================== *) + +(** Trivial lemmas without axiom *) + +Lemma wB_diff_0 : wB <> 0. +Proof. exact (fun x => let 'eq_refl := x in idProp). Qed. + +Lemma wB_pos : 0 < wB. +Proof. reflexivity. Qed. + +Lemma to_Z_0 : [|0|] = 0. +Proof. reflexivity. Qed. + +Lemma to_Z_1 : [|1|] = 1. +Proof. reflexivity. Qed. + +(* Notations *) +Local Open Scope Z_scope. + +Notation "[+| c |]" := + (interp_carry 1 wB to_Z c) (at level 0, c at level 99) : int63_scope. + +Notation "[-| c |]" := + (interp_carry (-1) wB to_Z c) (at level 0, c at level 99) : int63_scope. + +Notation "[|| x ||]" := + (zn2z_to_Z wB to_Z x) (at level 0, x at level 99) : int63_scope. + +(* Bijection : int63 <-> Bvector size *) + +Axiom of_to_Z : forall x, of_Z [| x |] = x. + +Notation "'φ' x" := [| x |] (at level 0) : int63_scope. + +Lemma can_inj {rT aT} {f: aT -> rT} {g: rT -> aT} (K: forall a, g (f a) = a) {a a'} (e: f a = f a') : a = a'. +Proof. generalize (K a) (K a'). congruence. Qed. + +Lemma to_Z_inj x y : φ x = φ y → x = y. +Proof. exact (λ e, can_inj of_to_Z e). Qed. + +(** Specification of logical operations *) +Local Open Scope Z_scope. +Axiom lsl_spec : forall x p, [| x << p |] = [| x |] * 2 ^ [| p |] mod wB. + +Axiom lsr_spec : forall x p, [|x >> p|] = [|x|] / 2 ^ [|p|]. + +Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i. + +Axiom lor_spec: forall x y i, bit (x lor y) i = bit x i || bit y i. + +Axiom lxor_spec: forall x y i, bit (x lxor y) i = xorb (bit x i) (bit y i). + +(** Specification of basic opetations *) + +(* Arithmetic modulo operations *) + +(* Remarque : les axiomes seraient plus simple si on utilise of_Z a la place : + exemple : add_spec : forall x y, of_Z (x + y) = of_Z x + of_Z y. *) + +Axiom add_spec : forall x y, [|x + y|] = ([|x|] + [|y|]) mod wB. + +Axiom sub_spec : forall x y, [|x - y|] = ([|x|] - [|y|]) mod wB. + +Axiom mul_spec : forall x y, [| x * y |] = [|x|] * [|y|] mod wB. + +Axiom mulc_spec : forall x y, [|x|] * [|y|] = [|fst (mulc x y)|] * wB + [|snd (mulc x y)|]. + +Axiom div_spec : forall x y, [|x / y|] = [|x|] / [|y|]. + +Axiom mod_spec : forall x y, [|x \% y|] = [|x|] mod [|y|]. + +(* Comparisons *) +Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +Axiom eqb_refl : forall x, (x == x)%int63 = true. + +Axiom ltb_spec : forall x y, (x < y)%int63 = true <-> [|x|] < [|y|]. + +Axiom leb_spec : forall x y, (x <= y)%int63 = true <-> [|x|] <= [|y|]. + +(** Exotic operations *) + +(** I should add the definition (like for compare) *) +Primitive head0 := #int63_head0. +Primitive tail0 := #int63_tail0. + +(** Axioms on operations which are just short cut *) + +Axiom compare_def_spec : forall x y, compare x y = compare_def x y. + +Axiom head0_spec : forall x, 0 < [|x|] -> + wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB. + +Axiom tail0_spec : forall x, 0 < [|x|] -> + (exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]))%Z. + +Axiom addc_def_spec : forall x y, (x +c y)%int63 = addc_def x y. + +Axiom addcarryc_def_spec : forall x y, addcarryc x y = addcarryc_def x y. + +Axiom subc_def_spec : forall x y, (x -c y)%int63 = subc_def x y. + +Axiom subcarryc_def_spec : forall x y, subcarryc x y = subcarryc_def x y. + +Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y. + +Axiom diveucl_21_spec : forall a1 a2 b, + let (q,r) := diveucl_21 a1 a2 b in + ([|q|],[|r|]) = Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|]. + +Axiom addmuldiv_def_spec : forall p x y, + addmuldiv p x y = addmuldiv_def p x y. + +(** Square root functions using newton iteration **) +Local Open Scope int63_scope. + +Definition sqrt_step (rec: int -> int -> int) (i j: int) := + let quo := i / j in + if quo < j then rec i ((j + quo) >> 1) + else j. + +Definition iter_sqrt := + Eval lazy beta delta [sqrt_step] in + fix iter_sqrt (n: nat) (rec: int -> int -> int) + (i j: int) {struct n} : int := + sqrt_step + (fun i j => match n with + O => rec i j + | S n => (iter_sqrt n (iter_sqrt n rec)) i j + end) i j. + +Definition sqrt i := + match compare 1 i with + Gt => 0 + | Eq => 1 + | Lt => iter_sqrt size (fun i j => j) i (i >> 1) + end. + +Definition high_bit := 1 << (digits - 1). + +Definition sqrt2_step (rec: int -> int -> int -> int) + (ih il j: int) := + if ih < j then + let (quo,_) := diveucl_21 ih il j in + if quo < j then + match j +c quo with + | C0 m1 => rec ih il (m1 >> 1) + | C1 m1 => rec ih il ((m1 >> 1) + high_bit) + end + else j + else j. + +Definition iter2_sqrt := + Eval lazy beta delta [sqrt2_step] in + fix iter2_sqrt (n: nat) + (rec: int -> int -> int -> int) + (ih il j: int) {struct n} : int := + sqrt2_step + (fun ih il j => + match n with + | O => rec ih il j + | S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j + end) ih il j. + +Definition sqrt2 ih il := + let s := iter2_sqrt size (fun ih il j => j) ih il max_int in + let (ih1, il1) := mulc s s in + match il -c il1 with + | C0 il2 => + if ih1 < ih then (s, C1 il2) else (s, C0 il2) + | C1 il2 => + if ih1 < (ih - 1) then (s, C1 il2) else (s, C0 il2) + end. + +(** Gcd **) +Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} := + match guard with + | O => 1 + | S p => if j == 0 then i else gcd_rec p j (i \% j) + end. + +Definition gcd := gcd_rec (2*size). + +(** equality *) +Lemma eqb_complete : forall x y, x = y -> (x == y) = true. +Proof. + intros x y H; rewrite -> H, eqb_refl;trivial. +Qed. + +Lemma eqb_spec : forall x y, (x == y) = true <-> x = y. +Proof. + split;auto using eqb_correct, eqb_complete. +Qed. + +Lemma eqb_false_spec : forall x y, (x == y) = false <-> x <> y. +Proof. + intros;rewrite <- not_true_iff_false, eqb_spec;split;trivial. +Qed. + +Lemma eqb_false_complete : forall x y, x <> y -> (x == y) = false. +Proof. + intros x y;rewrite eqb_false_spec;trivial. +Qed. + +Lemma eqb_false_correct : forall x y, (x == y) = false -> x <> y. +Proof. + intros x y;rewrite eqb_false_spec;trivial. +Qed. + +Definition eqs (i j : int) : {i = j} + { i <> j } := + (if i == j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) + then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true)) + else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false))) + (eqb_correct i j) + (eqb_false_correct i j). + +Lemma eq_dec : forall i j:int, i = j \/ i <> j. +Proof. + intros i j;destruct (eqs i j);auto. +Qed. + +(* Extra function on equality *) + +Definition cast i j := + (if i == j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j)) + then fun Heq : true = true -> i = j => + Some + (fun (P : int -> Type) (Hi : P i) => + match Heq (eq_refl true) in (_ = y) return (P y) with + | eq_refl => Hi + end) + else fun _ : false = true -> i = j => None) (eqb_correct i j). + +Lemma cast_refl : forall i, cast i i = Some (fun P H => H). +Proof. + unfold cast;intros. + generalize (eqb_correct i i). + rewrite eqb_refl;intros. + rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. +Qed. + +Lemma cast_diff : forall i j, i == j = false -> cast i j = None. +Proof. + intros;unfold cast;intros; generalize (eqb_correct i j). + rewrite H;trivial. +Qed. + +Definition eqo i j := + (if i == j as b return ((b = true -> i = j) -> option (i=j)) + then fun Heq : true = true -> i = j => + Some (Heq (eq_refl true)) + else fun _ : false = true -> i = j => None) (eqb_correct i j). + +Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i). +Proof. + unfold eqo;intros. + generalize (eqb_correct i i). + rewrite eqb_refl;intros. + rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. +Qed. + +Lemma eqo_diff : forall i j, i == j = false -> eqo i j = None. +Proof. + unfold eqo;intros; generalize (eqb_correct i j). + rewrite H;trivial. +Qed. + +(** Comparison *) + +Lemma eqbP x y : reflect ([| x |] = [| y |]) (x == y). +Proof. apply iff_reflect; rewrite eqb_spec; split; [ apply to_Z_inj | apply f_equal ]. Qed. + +Lemma ltbP x y : reflect ([| x |] < [| y |])%Z (x < y). +Proof. apply iff_reflect; symmetry; apply ltb_spec. Qed. + +Lemma lebP x y : reflect ([| x |] <= [| y |])%Z (x ≤ y). +Proof. apply iff_reflect; symmetry; apply leb_spec. Qed. + +Lemma compare_spec x y : compare x y = ([|x|] ?= [|y|])%Z. +Proof. + rewrite compare_def_spec; unfold compare_def. + case ltbP; [ auto using Z.compare_lt_iff | intros hge ]. + case eqbP; [ now symmetry; apply Z.compare_eq_iff | intros hne ]. + symmetry; apply Z.compare_gt_iff; lia. +Qed. + +Lemma is_zero_spec x : is_zero x = true <-> x = 0%int63. +Proof. apply eqb_spec. Qed. + +Lemma diveucl_spec x y : + let (q,r) := diveucl x y in + ([| q |], [| r |]) = Z.div_eucl [| x |] [| y |]. +Proof. + rewrite diveucl_def_spec; unfold diveucl_def; rewrite div_spec, mod_spec; unfold Z.div, Zmod. + destruct (Z.div_eucl [| x |] [| y |]); trivial. +Qed. + +Local Open Scope Z_scope. +(** Addition *) +Lemma addc_spec x y : [+| x +c y |] = [| x |] + [| y |]. +Proof. + rewrite addc_def_spec; unfold addc_def, interp_carry. + pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). + case ltbP; rewrite add_spec. + case (Z_lt_ge_dec ([| x |] + [| y |]) wB). + intros k; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] - wB)); lia. + case (Z_lt_ge_dec ([| x |] + [| y |]) wB). + intros k; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] - wB)); lia. +Qed. + +Lemma succ_spec x : [| succ x |] = ([| x |] + 1) mod wB. +Proof. apply add_spec. Qed. + +Lemma succc_spec x : [+| succc x |] = [| x |] + 1. +Proof. apply addc_spec. Qed. + +Lemma addcarry_spec x y : [| addcarry x y |] = ([| x |] + [| y |] + 1) mod wB. +Proof. unfold addcarry; rewrite -> !add_spec, Zplus_mod_idemp_l; trivial. Qed. + +Lemma addcarryc_spec x y : [+| addcarryc x y |] = [| x |] + [| y |] + 1. +Proof. + rewrite addcarryc_def_spec; unfold addcarryc_def, interp_carry. + pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). + case lebP; rewrite addcarry_spec. + case (Z_lt_ge_dec ([| x |] + [| y |] + 1) wB). + intros hlt; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] + 1 - wB)); lia. + case (Z_lt_ge_dec ([| x |] + [| y |] + 1) wB). + intros hlt; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ 1 ([| x |] + [| y |] + 1 - wB)); lia. +Qed. + +(** Subtraction *) +Lemma subc_spec x y : [-| x -c y |] = [| x |] - [| y |]. +Proof. + rewrite subc_def_spec; unfold subc_def; unfold interp_carry. + pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). + case lebP. + intros hle; rewrite sub_spec, Z.mod_small; lia. + intros hgt; rewrite sub_spec, <- (Zmod_unique _ wB (-1) ([| x |] - [| y |] + wB)); lia. +Qed. + +Lemma pred_spec x : [| pred x |] = ([| x |] - 1) mod wB. +Proof. apply sub_spec. Qed. + +Lemma predc_spec x : [-| predc x |] = [| x |] - 1. +Proof. apply subc_spec. Qed. + +Lemma oppc_spec x : [-| oppc x |] = - [| x |]. +Proof. unfold oppc; rewrite -> subc_spec, to_Z_0; trivial. Qed. + +Lemma opp_spec x : [|- x |] = - [| x |] mod wB. +Proof. unfold opp; rewrite -> sub_spec, to_Z_0; trivial. Qed. + +Lemma oppcarry_spec x : [| oppcarry x |] = wB - [| x |] - 1. +Proof. + unfold oppcarry; rewrite sub_spec. + rewrite <- Zminus_plus_distr, Zplus_comm, Zminus_plus_distr. + apply Zmod_small. + generalize (to_Z_bounded x); auto with zarith. +Qed. + +Lemma subcarry_spec x y : [| subcarry x y |] = ([| x |] - [| y |] - 1) mod wB. +Proof. unfold subcarry; rewrite !sub_spec, Zminus_mod_idemp_l; trivial. Qed. + +Lemma subcarryc_spec x y : [-| subcarryc x y |] = [| x |] - [| y |] - 1. +Proof. + rewrite subcarryc_def_spec; unfold subcarryc_def, interp_carry; fold (subcarry x y). + pose proof (to_Z_bounded x); pose proof (to_Z_bounded y). + case ltbP; rewrite subcarry_spec. + intros hlt; rewrite Zmod_small; lia. + intros hge; rewrite <- (Zmod_unique _ _ (-1) ([| x |] - [| y |] - 1 + wB)); lia. +Qed. + +(** GCD *) +Lemma to_Z_gcd : forall i j, [| gcd i j |] = Zgcdn (2 * size) [| j |] [| i |]. +Proof. + unfold gcd. + elim (2*size)%nat. reflexivity. + intros n ih i j; simpl. + pose proof (to_Z_bounded j) as hj; pose proof (to_Z_bounded i). + case eqbP; rewrite to_Z_0. + intros ->; rewrite Z.abs_eq; lia. + intros hne; rewrite ih; clear ih. + rewrite <- mod_spec. + revert hj hne; case [| j |]; intros; lia. +Qed. + +Lemma gcd_spec a b : Zis_gcd [| a |] [| b |] [| gcd a b |]. +Proof. + rewrite to_Z_gcd. + apply Zis_gcd_sym. + apply Zgcdn_is_gcd. + unfold Zgcd_bound. + generalize (to_Z_bounded b). + destruct [|b|]. + unfold size; auto with zarith. + intros (_,H). + cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. + intros (H,_); compute in H; elim H; auto. +Qed. + +(** Head0, Tail0 *) +Lemma head00_spec x : [| x |] = 0 -> [| head0 x |] = [| digits |]. +Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed. + +Lemma tail00_spec x : [| x |] = 0 -> [|tail0 x|] = [|digits|]. +Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed. + +Infix "≡" := (eqm wB) (at level 80) : int63_scope. + +Lemma eqm_mod x y : x mod wB ≡ y mod wB → x ≡ y. +Proof. + intros h. + eapply (eqm_trans). + apply eqm_sym; apply Zmod_eqm. + apply (eqm_trans _ _ _ _ h). + apply Zmod_eqm. +Qed. + +Lemma eqm_sub x y : x ≡ y → x - y ≡ 0. +Proof. intros h; unfold eqm; rewrite Zminus_mod, h, Z.sub_diag; reflexivity. Qed. + +Lemma eqmE x y : x ≡ y → ∃ k, x - y = k * wB. +Proof. + intros h. + exact (Zmod_divide (x - y) wB (λ e, let 'eq_refl := e in I) (eqm_sub _ _ h)). +Qed. + +Lemma eqm_subE x y : x ≡ y ↔ x - y ≡ 0. +Proof. + split. apply eqm_sub. + intros h; case (eqmE _ _ h); clear h; intros q h. + assert (y = x - q * wB) by lia. + clear h; subst y. + unfold eqm; rewrite Zminus_mod, Z_mod_mult, Z.sub_0_r, Zmod_mod; reflexivity. +Qed. + +Lemma int_eqm x y : x = y → φ x ≡ φ y. +Proof. unfold eqm; intros ->; reflexivity. Qed. + +Lemma eqmI x y : φ x ≡ φ y → x = y. +Proof. + unfold eqm. + repeat rewrite Zmod_small by apply to_Z_bounded. + apply to_Z_inj. +Qed. + +(* ADD *) +Lemma add_assoc x y z: (x + (y + z) = (x + y) + z)%int63. +Proof. + apply to_Z_inj; rewrite !add_spec. + rewrite -> Zplus_mod_idemp_l, Zplus_mod_idemp_r, Zplus_assoc; auto. +Qed. + +Lemma add_comm x y: (x + y = y + x)%int63. +Proof. + apply to_Z_inj; rewrite -> !add_spec, Zplus_comm; auto. +Qed. + +Lemma add_le_r m n: + if (n <= m + n)%int63 then ([|m|] + [|n|] < wB)%Z else (wB <= [|m|] + [|n|])%Z. +Proof. + case (to_Z_bounded m); intros H1m H2m. + case (to_Z_bounded n); intros H1n H2n. + case (Zle_or_lt wB ([|m|] + [|n|])); intros H. + assert (H1: ([| m + n |] = [|m|] + [|n|] - wB)%Z). + rewrite add_spec. + replace (([|m|] + [|n|]) mod wB)%Z with (((([|m|] + [|n|]) - wB) + wB) mod wB)%Z. + rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. + rewrite !Zmod_small; auto with zarith. + apply f_equal2 with (f := Zmod); auto with zarith. + case_eq (n <= m + n)%int63; auto. + rewrite leb_spec, H1; auto with zarith. + assert (H1: ([| m + n |] = [|m|] + [|n|])%Z). + rewrite add_spec, Zmod_small; auto with zarith. + replace (n <= m + n)%int63 with true; auto. + apply sym_equal; rewrite leb_spec, H1; auto with zarith. +Qed. + +Lemma add_cancel_l x y z : (x + y = x + z)%int63 -> y = z. +Proof. + intros h; apply int_eqm in h; rewrite !add_spec in h; apply eqm_mod, eqm_sub in h. + replace (_ + _ - _) with (φ(y) - φ(z)) in h by lia. + rewrite <- eqm_subE in h. + apply eqmI, h. +Qed. + +Lemma add_cancel_r x y z : (y + x = z + x)%int63 -> y = z. +Proof. + rewrite !(fun t => add_comm t x); intros Hl; apply (add_cancel_l x); auto. +Qed. + +Coercion b2i (b: bool) : int := if b then 1%int63 else 0%int63. + +(* LSR *) +Lemma lsr0 i : 0 >> i = 0%int63. +Proof. apply to_Z_inj; rewrite lsr_spec; reflexivity. Qed. + +Lemma lsr_0_r i: i >> 0 = i. +Proof. apply to_Z_inj; rewrite lsr_spec, Zdiv_1_r; exact eq_refl. Qed. + +Lemma lsr_1 n : 1 >> n = (n == 0). +Proof. + case eqbP. + intros h; rewrite (to_Z_inj _ _ h), lsr_0_r; reflexivity. + intros Hn. + assert (H1n : (1 >> n = 0)%int63); auto. + apply to_Z_inj; rewrite lsr_spec. + apply Zdiv_small; rewrite to_Z_1; split; auto with zarith. + change 1%Z with (2^0)%Z. + apply Zpower_lt_monotone; split; auto with zarith. + rewrite to_Z_0 in Hn. + generalize (to_Z_bounded n). + lia. +Qed. + +Lemma lsr_add i m n: ((i >> m) >> n = if n <= m + n then i >> (m + n) else 0)%int63. +Proof. + case (to_Z_bounded m); intros H1m H2m. + case (to_Z_bounded n); intros H1n H2n. + case (to_Z_bounded i); intros H1i H2i. + generalize (add_le_r m n); case (n <= m + n)%int63; intros H. + apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. + rewrite add_spec, Zmod_small; auto with zarith. + apply to_Z_inj; rewrite -> !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. + apply Zdiv_small. split; [ auto with zarith | ]. + eapply Z.lt_le_trans; [ | apply Zpower2_le_lin ]; auto with zarith. +Qed. + +Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. +Proof. + apply to_Z_inj. + rewrite -> add_spec, !lsl_spec, add_spec. + rewrite -> Zmult_mod_idemp_l, <-Zplus_mod. + apply f_equal2 with (f := Zmod); auto with zarith. +Qed. + +(* LSL *) +Lemma lsl0 i: 0 << i = 0%int63. +Proof. + apply to_Z_inj. + generalize (lsl_spec 0 i). + rewrite to_Z_0, Zmult_0_l, Zmod_0_l; auto. +Qed. + +Lemma lsl0_r i : i << 0 = i. +Proof. + apply to_Z_inj. + rewrite -> lsl_spec, to_Z_0, Z.mul_1_r. + apply Zmod_small; apply (to_Z_bounded i). +Qed. + +Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. +Proof. + apply to_Z_inj; rewrite -> !lsl_spec, !add_spec, Zmult_mod_idemp_l. + rewrite -> !lsl_spec, <-Zplus_mod. + apply f_equal2 with (f := Zmod); auto with zarith. +Qed. + +Lemma lsr_M_r x i (H: (digits <= i = true)%int63) : x >> i = 0%int63. +Proof. + apply to_Z_inj. + rewrite lsr_spec, to_Z_0. + case (to_Z_bounded x); intros H1x H2x. + case (to_Z_bounded digits); intros H1d H2d. + rewrite -> leb_spec in H. + apply Zdiv_small; split; [ auto | ]. + apply (Z.lt_le_trans _ _ _ H2x). + unfold wB; change (Z_of_nat size) with [|digits|]. + apply Zpower_le_monotone; auto with zarith. +Qed. + +(* BIT *) +Lemma bit_0_spec i: [|bit i 0|] = [|i|] mod 2. +Proof. + unfold bit, is_zero. rewrite lsr_0_r. + assert (Hbi: ([|i|] mod 2 < 2)%Z). + apply Z_mod_lt; auto with zarith. + case (to_Z_bounded i); intros H1i H2i. + case (Zmod_le_first [|i|] 2); auto with zarith; intros H3i H4i. + assert (H2b: (0 < 2 ^ [|digits - 1|])%Z). + apply Zpower_gt_0; auto with zarith. + case (to_Z_bounded (digits -1)); auto with zarith. + assert (H: [|i << (digits -1)|] = ([|i|] mod 2 * 2^ [|digits -1|])%Z). + rewrite lsl_spec. + rewrite -> (Z_div_mod_eq [|i|] 2) at 1; auto with zarith. + rewrite -> Zmult_plus_distr_l, <-Zplus_mod_idemp_l. + rewrite -> (Zmult_comm 2), <-Zmult_assoc. + replace (2 * 2 ^ [|digits - 1|])%Z with wB; auto. + rewrite Z_mod_mult, Zplus_0_l; apply Zmod_small. + split; auto with zarith. + replace wB with (2 * 2 ^ [|digits -1|])%Z; auto. + apply Zmult_lt_compat_r; auto with zarith. + case (Zle_lt_or_eq 0 ([|i|] mod 2)); auto with zarith; intros Hi. + 2: generalize H; rewrite <-Hi, Zmult_0_l. + 2: replace 0%Z with [|0|]; auto. + 2: now case eqbP. + generalize H; replace ([|i|] mod 2) with 1%Z; auto with zarith. + rewrite Zmult_1_l. + intros H1. + assert (H2: [|i << (digits - 1)|] <> [|0|]). + replace [|0|] with 0%Z; auto with zarith. + now case eqbP. +Qed. + +Lemma bit_split i : ( i = (i >> 1 ) << 1 + bit i 0)%int63. +Proof. + apply to_Z_inj. + rewrite -> add_spec, lsl_spec, lsr_spec, bit_0_spec, Zplus_mod_idemp_l. + replace (2 ^ [|1|]) with 2%Z; auto with zarith. + rewrite -> Zmult_comm, <-Z_div_mod_eq; auto with zarith. + rewrite Zmod_small; auto; case (to_Z_bounded i); auto. +Qed. + +Lemma bit_lsr x i j : + (bit (x >> i) j = if j <= i + j then bit x (i + j) else false)%int63. +Proof. + unfold bit; rewrite lsr_add; case (_ ≤ _); auto. +Qed. + +Lemma bit_b2i (b: bool) i : bit b i = (i == 0) && b. +Proof. + case b; unfold bit; simpl b2i. + rewrite lsr_1; case (i == 0); auto. + rewrite lsr0, lsl0, andb_false_r; auto. +Qed. + +Lemma bit_1 n : bit 1 n = (n == 0). +Proof. + unfold bit; rewrite lsr_1. + case (_ == _); simpl; auto. +Qed. + +Local Hint Resolve Z.lt_gt Z.div_pos : zarith. + +Lemma to_Z_split x : [|x|] = [|(x >> 1)|] * 2 + [|bit x 0|]. +Proof. + case (to_Z_bounded x); intros H1x H2x. + case (to_Z_bounded (bit x 0)); intros H1b H2b. + assert (F1: 0 <= [|x >> 1|] < wB/2). + rewrite -> lsr_spec, to_Z_1, Z.pow_1_r. split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite -> (bit_split x) at 1. + rewrite -> add_spec, Zmod_small, lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; + split; auto with zarith. + change wB with ((wB/2)*2); auto with zarith. + rewrite -> lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto with zarith. + change wB with ((wB/2)*2); auto with zarith. + rewrite -> lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto with zarith. + 2: change wB with ((wB/2)*2); auto with zarith. + change wB with (((wB/2 - 1) * 2 + 1) + 1). + assert ([|bit x 0|] <= 1); auto with zarith. + case bit; discriminate. +Qed. + +Lemma bit_M i n (H: (digits <= n = true)%int63): bit i n = false. +Proof. unfold bit; rewrite lsr_M_r; auto. Qed. + +Lemma bit_half i n (H: (n < digits = true)%int63) : bit (i>>1) n = bit i (n+1). +Proof. + unfold bit. + rewrite lsr_add. + case_eq (n <= (1 + n))%int63. + replace (1+n)%int63 with (n+1)%int63; [auto|idtac]. + apply to_Z_inj; rewrite !add_spec, Zplus_comm; auto. + intros H1; assert (H2: n = max_int). + 2: generalize H; rewrite H2; discriminate. + case (to_Z_bounded n); intros H1n H2n. + case (Zle_lt_or_eq [|n|] (wB - 1)); auto with zarith; + intros H2; apply to_Z_inj; auto. + generalize (add_le_r 1 n); rewrite H1. + change [|max_int|] with (wB - 1)%Z. + replace [|1|] with 1%Z; auto with zarith. +Qed. + +Lemma bit_ext i j : (forall n, bit i n = bit j n) -> i = j. +Proof. + case (to_Z_bounded j); case (to_Z_bounded i). + unfold wB; revert i j; elim size. + simpl; intros i j ???? _; apply to_Z_inj; lia. + intros n ih i j. + rewrite Nat2Z.inj_succ, Z.pow_succ_r by auto with zarith. + intros hi1 hi2 hj1 hj2 hext. + rewrite (bit_split i), (bit_split j), hext. + do 2 f_equal; apply ih; clear ih. + 1, 3: apply to_Z_bounded. + 1, 2: rewrite lsr_spec; auto using Z_lt_div2. + intros b. + case (Zle_or_lt [|digits|] [|b|]). + rewrite <- leb_spec; intros; rewrite !bit_M; auto. + rewrite <- ltb_spec; intros; rewrite !bit_half; auto. +Qed. + +Lemma bit_lsl x i j : bit (x << i) j = +(if (j < i) || (digits <= j) then false else bit x (j - i))%int63. +Proof. + assert (F1: 1 >= 0) by discriminate. + case_eq (digits <= j)%int63; intros H. + rewrite orb_true_r, bit_M; auto. + set (d := [|digits|]). + case (Zle_or_lt d [|j|]); intros H1. + case (leb_spec digits j); rewrite H; auto with zarith. + intros _ HH; generalize (HH H1); discriminate. + clear H. + generalize (ltb_spec j i); case ltb; intros H2; unfold bit; simpl. + assert (F2: ([|j|] < [|i|])%Z) by (case H2; auto); clear H2. + replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. + case (to_Z_bounded j); intros H1j H2j. + apply sym_equal; rewrite is_zero_spec; apply to_Z_inj. + rewrite lsl_spec, lsr_spec, lsl_spec. + replace wB with (2^d); auto. + pattern d at 1; replace d with ((d - ([|j|] + 1)) + ([|j|] + 1))%Z by ring. + rewrite Zpower_exp; auto with zarith. + replace [|i|] with (([|i|] - ([|j|] + 1)) + ([|j|] + 1))%Z by ring. + rewrite -> Zpower_exp, Zmult_assoc; auto with zarith. + rewrite Zmult_mod_distr_r. + rewrite -> Zplus_comm, Zpower_exp, !Zmult_assoc; auto with zarith. + rewrite -> Z_div_mult_full; auto with zarith. + rewrite <-Zmult_assoc, <-Zpower_exp; auto with zarith. + replace (1 + [|digits - 1|])%Z with d; auto with zarith. + rewrite Z_mod_mult; auto. + case H2; intros _ H3; case (Zle_or_lt [|i|] [|j|]); intros F2. + 2: generalize (H3 F2); discriminate. + clear H2 H3. + apply f_equal with (f := negb). + apply f_equal with (f := is_zero). + apply to_Z_inj. + rewrite -> !lsl_spec, !lsr_spec, !lsl_spec. + pattern wB at 2 3; replace wB with (2^(1+ [|digits - 1|])); auto. + rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. + rewrite !Zmult_mod_distr_r. + apply f_equal2 with (f := Zmult); auto. + replace wB with (2^ d); auto with zarith. + replace d with ((d - [|i|]) + [|i|])%Z by ring. + case (to_Z_bounded i); intros H1i H2i. + rewrite Zpower_exp; auto with zarith. + rewrite Zmult_mod_distr_r. + case (to_Z_bounded j); intros H1j H2j. + replace [|j - i|] with ([|j|] - [|i|])%Z. + 2: rewrite sub_spec, Zmod_small; auto with zarith. + set (d1 := (d - [|i|])%Z). + set (d2 := ([|j|] - [|i|])%Z). + pattern [|j|] at 1; + replace [|j|] with (d2 + [|i|])%Z. + 2: unfold d2; ring. + rewrite -> Zpower_exp; auto with zarith. + rewrite -> Zdiv_mult_cancel_r. + 2: generalize (Zpower2_lt_lin [| i |] H1i); auto with zarith. + rewrite -> (Z_div_mod_eq [|x|] (2^d1)) at 2; auto with zarith. + pattern d1 at 2; + replace d1 with (d2 + (1+ (d - [|j|] - 1)))%Z + by (unfold d1, d2; ring). + rewrite Zpower_exp; auto with zarith. + rewrite <-Zmult_assoc, Zmult_comm. + rewrite Zdiv.Z_div_plus_full_l; auto with zarith. + rewrite Zpower_exp, Z.pow_1_r; auto with zarith. + rewrite <-Zplus_mod_idemp_l. + rewrite <-!Zmult_assoc, Zmult_comm, Z_mod_mult, Zplus_0_l; auto. +Qed. + +(* LOR *) +Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i). +Proof. + apply bit_ext; intros n. + rewrite -> lor_spec, !bit_lsr, lor_spec. + case (_ <= _)%int63; auto. +Qed. + +Lemma lor_le x y : (y <= x lor y)%int63 = true. +Proof. + generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y. + unfold wB; elim size. + replace (2^Z_of_nat 0) with 1%Z; auto with zarith. + intros x y Hx Hy; replace x with 0%int63. + replace y with 0%int63; auto. + apply to_Z_inj; rewrite to_Z_0; auto with zarith. + apply to_Z_inj; rewrite to_Z_0; auto with zarith. + intros n IH x y; rewrite inj_S. + unfold Z.succ; rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. + intros Hx Hy. + rewrite leb_spec. + rewrite -> (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)). + assert ([|y>>1|] <= [|(x lor y) >> 1|]). + rewrite -> lor_lsr, <-leb_spec; apply IH. + rewrite -> lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite -> lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + assert ([|bit y 0|] <= [|bit (x lor y) 0|]); auto with zarith. + rewrite lor_spec; do 2 case bit; try discriminate. +Qed. + +Lemma bit_0 n : bit 0 n = false. +Proof. unfold bit; rewrite lsr0; auto. Qed. + +Lemma bit_add_or x y: + (forall n, bit x n = true -> bit y n = true -> False) <-> (x + y)%int63= x lor y. +Proof. + generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y. + unfold wB; elim size. + replace (2^Z_of_nat 0) with 1%Z; auto with zarith. + intros x y Hx Hy; replace x with 0%int63. + replace y with 0%int63. + split; auto; intros _ n; rewrite !bit_0; discriminate. + apply to_Z_inj; rewrite to_Z_0; auto with zarith. + apply to_Z_inj; rewrite to_Z_0; auto with zarith. + intros n IH x y; rewrite inj_S. + unfold Z.succ; rewrite Zpower_exp, Z.pow_1_r; auto with zarith. + intros Hx Hy. + split. + intros Hn. + assert (F1: ((x >> 1) + (y >> 1))%int63 = (x >> 1) lor (y >> 1)). + apply IH. + rewrite lsr_spec, Z.pow_1_r; split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite lsr_spec, Z.pow_1_r; split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + intros m H1 H2. + case_eq (digits <= m)%int63; [idtac | rewrite <- not_true_iff_false]; + intros Heq. + rewrite bit_M in H1; auto; discriminate. + rewrite leb_spec in Heq. + apply (Hn (m + 1)%int63); + rewrite <-bit_half; auto; rewrite ltb_spec; auto with zarith. + rewrite (bit_split (x lor y)), lor_lsr, <- F1, lor_spec. + replace (b2i (bit x 0 || bit y 0)) with (bit x 0 + bit y 0)%int63. + 2: generalize (Hn 0%int63); do 2 case bit; auto; intros [ ]; auto. + rewrite lsl_add_distr. + rewrite (bit_split x) at 1; rewrite (bit_split y) at 1. + rewrite <-!add_assoc; apply f_equal2 with (f := add); auto. + rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add); auto. + rewrite add_comm; auto. + intros Heq. + generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. + generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq. + rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm, + <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsr_add_distr. + rewrite (bit_split (x lor y)), lor_spec. + intros Heq. + assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)). + assert (F1: (2 | wB)) by (apply Zpower_divide; apply refl_equal). + assert (F2: 0 < wB) by (apply refl_equal). + assert (F3: [|bit x 0 + bit y 0|] mod 2 = [|bit x 0 || bit y 0|] mod 2). + apply trans_equal with (([|(x>>1 + y>>1) << 1|] + [|bit x 0 + bit y 0|]) mod 2). + rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith. + rewrite Z.pow_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith. + rewrite (Zmod_div_mod 2 wB), <-add_spec, Heq; auto with zarith. + rewrite add_spec, <-Zmod_div_mod; auto with zarith. + rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith. + rewrite Z.pow_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith. + generalize F3; do 2 case bit; try discriminate; auto. + case (IH (x >> 1) (y >> 1)). + rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + intros _ HH m; case (to_Z_bounded m); intros H1m H2m. + case_eq (digits <= m)%int63. + intros Hlm; rewrite bit_M; auto; discriminate. + rewrite <- not_true_iff_false, leb_spec; intros Hlm. + case (Zle_lt_or_eq 0 [|m|]); auto; intros Hm. + replace m with ((m -1) + 1)%int63. + rewrite <-(bit_half x), <-(bit_half y); auto with zarith. + apply HH. + rewrite <-lor_lsr. + assert (0 <= [|bit (x lor y) 0|] <= 1) by (case bit; split; discriminate). + rewrite F in Heq; generalize (add_cancel_r _ _ _ Heq). + intros Heq1; apply to_Z_inj. + generalize (f_equal to_Z Heq1); rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small. + rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto with zarith. + case (to_Z_bounded (x lor y)); intros H1xy H2xy. + rewrite lsr_spec, to_Z_1, Z.pow_1_r; auto with zarith. + change wB with ((wB/2)*2); split; auto with zarith. + assert ([|x lor y|] / 2 < wB / 2); auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + split. + case (to_Z_bounded (x >> 1 + y >> 1)); auto with zarith. + rewrite add_spec. + apply Z.le_lt_trans with (([|x >> 1|] + [|y >> 1|]) * 2); auto with zarith. + case (Zmod_le_first ([|x >> 1|] + [|y >> 1|]) wB); auto with zarith. + case (to_Z_bounded (x >> 1)); case (to_Z_bounded (y >> 1)); auto with zarith. + generalize Hb; rewrite (to_Z_split x) at 1; rewrite (to_Z_split y) at 1. + case (to_Z_bounded (bit x 0)); case (to_Z_bounded (bit y 0)); auto with zarith. + rewrite ltb_spec, sub_spec, to_Z_1, Zmod_small; auto with zarith. + rewrite ltb_spec, sub_spec, to_Z_1, Zmod_small; auto with zarith. + apply to_Z_inj. + rewrite add_spec, sub_spec, Zplus_mod_idemp_l, to_Z_1, Zmod_small; auto with zarith. + pose proof (to_Z_inj 0 _ Hm); clear Hm; subst m. + intros hx hy; revert F; rewrite hx, hy; intros F. generalize (f_equal to_Z F). vm_compute. lia. +Qed. + +Lemma addmuldiv_spec x y p : + [| p |] <= [| digits |] -> + [| addmuldiv p x y |] = ([| x |] * (2 ^ [| p |]) + [| y |] / (2 ^ ([| digits |] - [| p |]))) mod wB. +Proof. + intros H. + assert (Fp := to_Z_bounded p); assert (Fd := to_Z_bounded digits). + rewrite addmuldiv_def_spec; unfold addmuldiv_def. + case (bit_add_or (x << p) (y >> (digits - p))); intros HH _. + rewrite <-HH, add_spec, lsl_spec, lsr_spec, Zplus_mod_idemp_l, sub_spec. + rewrite (fun x y => Zmod_small (x - y)); auto with zarith. + intros n; rewrite -> bit_lsl, bit_lsr. + generalize (add_le_r (digits - p) n). + case (_ ≤ _); try discriminate. + rewrite -> sub_spec, Zmod_small; auto with zarith; intros H1. + case_eq (n < p)%int63; try discriminate. + rewrite <- not_true_iff_false, ltb_spec; intros H2. + case (_ ≤ _); try discriminate. + intros _; rewrite bit_M; try discriminate. + rewrite -> leb_spec, add_spec, Zmod_small, sub_spec, Zmod_small; auto with zarith. + rewrite -> sub_spec, Zmod_small; auto with zarith. +Qed. + +(* is_even *) +Lemma is_even_bit i : is_even i = negb (bit i 0). +Proof. + unfold is_even. + replace (i land 1) with (b2i (bit i 0)). + case bit; auto. + apply bit_ext; intros n. + rewrite bit_b2i, land_spec, bit_1. + generalize (eqb_spec n 0). + case (n == 0); auto. + intros(H,_); rewrite andb_true_r, H; auto. + rewrite andb_false_r; auto. +Qed. + +Lemma is_even_spec x : if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. +Proof. +rewrite is_even_bit. +generalize (bit_0_spec x); case bit; simpl; auto. +Qed. + +Lemma is_even_0 : is_even 0 = true. +Proof. apply refl_equal. Qed. + +Lemma is_even_lsl_1 i : is_even (i << 1) = true. +Proof. + rewrite is_even_bit, bit_lsl; auto. +Qed. + +(* Sqrt *) + + (* Direct transcription of an old proof + of a fortran program in boyer-moore *) + +Ltac elim_div := + unfold Z.div, Z.modulo; + match goal with + | H : context[ Z.div_eucl ?X ?Y ] |- _ => + generalize dependent H; generalize (Z_div_mod_full X Y) ; case (Z.div_eucl X Y) + | |- context[ Z.div_eucl ?X ?Y ] => + generalize (Z_div_mod_full X Y) ; case (Z.div_eucl X Y) + end; unfold Remainder. + +Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2). +Proof. + case (Z_mod_lt a 2); auto with zarith. + intros H1; rewrite Zmod_eq_full; auto with zarith. +Qed. + +Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k -> + (j * k) + j <= ((j + k)/2 + 1) ^ 2. +Proof. + intros Hj; generalize Hj k; pattern j; apply natlike_ind; + auto; clear k j Hj. + intros _ k Hk; repeat rewrite Zplus_0_l. + apply Zmult_le_0_compat; generalize (Z_div_pos k 2); auto with zarith. + intros j Hj Hrec _ k Hk; pattern k; apply natlike_ind; auto; clear k Hk. + rewrite -> Zmult_0_r, Zplus_0_r, Zplus_0_l. + generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j)); + unfold Z.succ. + rewrite Z.pow_2_r, Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. + auto with zarith. + intros k Hk _. + replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1). + generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)). + unfold Z.succ; repeat rewrite Z.pow_2_r; + repeat rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. + repeat rewrite Zmult_1_l; repeat rewrite Zmult_1_r. + auto with zarith. + rewrite -> Zplus_comm, <- Z_div_plus_full_l; auto with zarith. + apply f_equal2; auto with zarith. +Qed. + +Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2. +Proof. + intros Hi Hj. + assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith). + refine (Z.lt_le_trans _ _ _ _ (sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij)). + pattern i at 1; rewrite -> (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith. +Qed. + +Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i/j < j -> (j + (i/j))/2 < j. +Proof. + intros Hi Hj; elim_div; intros q r [ ? hr ]; [ lia | subst i ]. + elim_div; intros a b [ h [ hb | ] ]; lia. +Qed. + +Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i. +Proof. + intros Hi Hj Hd; rewrite Z.pow_2_r. + apply Z.le_trans with (j * (i/j)); auto with zarith. + apply Z_mult_div_ge; auto with zarith. +Qed. + +Lemma sqrt_step_correct rec i j: + 0 < [|i|] -> 0 < [|j|] -> [|i|] < ([|j|] + 1) ^ 2 -> + 2 * [|j|] < wB -> + (forall j1 : int, + 0 < [|j1|] < [|j|] -> [|i|] < ([|j1|] + 1) ^ 2 -> + [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) -> + [|sqrt_step rec i j|] ^ 2 <= [|i|] < ([|sqrt_step rec i j|] + 1) ^ 2. +Proof. + assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt). + intros Hi Hj Hij H31 Hrec. + unfold sqrt_step. + case ltbP; rewrite div_spec. + - intros hlt. + assert ([| j + i / j|] = [|j|] + [|i|]/[|j|]) as hj. + rewrite add_spec, Zmod_small;rewrite div_spec; auto with zarith. + apply Hrec; rewrite lsr_spec, hj, to_Z_1; change (2 ^ 1) with 2. + + split; [ | apply sqrt_test_false;auto with zarith]. + replace ([|j|] + [|i|]/[|j|]) with (1 * 2 + (([|j|] - 2) + [|i|] / [|j|])) by ring. + rewrite Z_div_plus_full_l; auto with zarith. + assert (0 <= [|i|]/ [|j|]) by (apply Z_div_pos; auto with zarith). + assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / 2) ; auto with zarith. + apply Z.div_pos; [ | lia ]. + case (Zle_lt_or_eq 1 [|j|]); auto with zarith; intros Hj1. + rewrite <- Hj1, Zdiv_1_r; lia. + + apply sqrt_main;auto with zarith. + - split;[apply sqrt_test_true | ];auto with zarith. +Qed. + +Lemma iter_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] -> + [|i|] < ([|j|] + 1) ^ 2 -> 2 * [|j|] < wB -> + (forall j1, 0 < [|j1|] -> 2^(Z_of_nat n) + [|j1|] <= [|j|] -> + [|i|] < ([|j1|] + 1) ^ 2 -> 2 * [|j1|] < wB -> + [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) -> + [|iter_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter_sqrt n rec i j|] + 1) ^ 2. +Proof. + revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n. + intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct; auto with zarith. + intros; apply Hrec; auto with zarith. + rewrite Zpower_0_r; auto with zarith. + intros n Hrec rec i j Hi Hj Hij H31 HHrec. + apply sqrt_step_correct; auto. + intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. + intros j2 Hj2 H2j2 Hjp2 Hj31; apply Hrec; auto with zarith. + intros j3 Hj3 Hpj3. + apply HHrec; auto. + rewrite -> inj_S, Z.pow_succ_r. + apply Z.le_trans with (2 ^Z_of_nat n + [|j2|]); auto with zarith. + apply Zle_0_nat. +Qed. + +Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2. +Proof. + intros Hi. + assert (H1: 0 <= i - 2) by auto with zarith. + assert (H2: 1 <= (i / 2) ^ 2); auto with zarith. + replace i with (1* 2 + (i - 2)); auto with zarith. + rewrite Z.pow_2_r, Z_div_plus_full_l; auto with zarith. + generalize (sqr_pos ((i - 2)/ 2)) (Z_div_pos (i - 2) 2). + rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. + auto with zarith. + generalize (quotient_by_2 i). + rewrite -> Z.pow_2_r in H2 |- *; + repeat (rewrite Zmult_plus_distr_l || + rewrite Zmult_plus_distr_r || + rewrite Zmult_1_l || rewrite Zmult_1_r). + auto with zarith. +Qed. + +Lemma sqrt_spec : forall x, + [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. +Proof. + intros i; unfold sqrt. + rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1; + intros Hi; auto with zarith. + repeat rewrite Z.pow_2_r; auto with zarith. + apply iter_sqrt_correct; auto with zarith; + rewrite lsr_spec, to_Z_1; change (2^1) with 2; auto with zarith. + replace [|i|] with (1 * 2 + ([|i|] - 2))%Z; try ring. + assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; auto with zarith). + rewrite Z_div_plus_full_l; auto with zarith. + apply sqrt_init; auto. + assert (W:= Z_mult_div_ge [|i|] 2);assert (W':= to_Z_bounded i);auto with zarith. + intros j2 H1 H2; contradict H2; apply Zlt_not_le. + fold wB;assert (W:=to_Z_bounded i). + apply Z.le_lt_trans with ([|i|]); auto with zarith. + assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith). + apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith. + apply Z_mult_div_ge; auto with zarith. + case (to_Z_bounded i); repeat rewrite Z.pow_2_r; auto with zarith. +Qed. + +(* sqrt2 *) +Lemma sqrt2_step_def rec ih il j: + sqrt2_step rec ih il j = + if (ih < j)%int63 then + let quo := fst (diveucl_21 ih il j) in + if (quo < j)%int63 then + let m := + match j +c quo with + | C0 m1 => m1 >> 1 + | C1 m1 => (m1 >> 1 + 1 << (digits -1))%int63 + end in + rec ih il m + else j + else j. +Proof. + unfold sqrt2_step; case diveucl_21; intros;simpl. + case (j +c i);trivial. +Qed. + +Lemma sqrt2_lower_bound ih il j: + [|| WW ih il||] < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|]. +Proof. + intros H1. + case (to_Z_bounded j); intros Hbj _. + case (to_Z_bounded il); intros Hbil _. + case (to_Z_bounded ih); intros Hbih Hbih1. + assert (([|ih|] < [|j|] + 1)%Z); auto with zarith. + apply Zlt_square_simpl; auto with zarith. + simpl zn2z_to_Z in H1. + repeat rewrite <-Z.pow_2_r. + refine (Z.le_lt_trans _ _ _ _ H1). + apply Z.le_trans with ([|ih|] * wB)%Z;try rewrite Z.pow_2_r; auto with zarith. +Qed. + +Lemma div2_phi ih il j: + [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|]. +Proof. + generalize (diveucl_21_spec ih il j). + case diveucl_21; intros q r Heq. + simpl zn2z_to_Z;unfold Z.div;rewrite <- Heq;trivial. +Qed. + +Lemma sqrt2_step_correct rec ih il j: + 2 ^ (Z_of_nat (size - 2)) <= [|ih|] -> + 0 < [|j|] -> [|| WW ih il||] < ([|j|] + 1) ^ 2 -> + (forall j1, 0 < [|j1|] < [|j|] -> [|| WW ih il||] < ([|j1|] + 1) ^ 2 -> + [|rec ih il j1|] ^ 2 <= [||WW ih il||] < ([|rec ih il j1|] + 1) ^ 2) -> + [|sqrt2_step rec ih il j|] ^ 2 <= [||WW ih il ||] + < ([|sqrt2_step rec ih il j|] + 1) ^ 2. +Proof. + assert (Hp2: (0 < [|2|])%Z) by exact (refl_equal Lt). + intros Hih Hj Hij Hrec; rewrite sqrt2_step_def. + assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt2_lower_bound with il; auto). + case (to_Z_bounded ih); intros Hih1 _. + case (to_Z_bounded il); intros Hil1 _. + case (to_Z_bounded j); intros _ Hj1. + assert (Hp3: (0 < [||WW ih il||])). + simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith. + apply Zmult_lt_0_compat; auto with zarith. + refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. + cbv zeta. + case_eq (ih < j)%int63;intros Heq. + rewrite -> ltb_spec in Heq. + 2: rewrite <-not_true_iff_false, ltb_spec in Heq. + 2: split; auto. + 2: apply sqrt_test_true; auto with zarith. + 2: unfold zn2z_to_Z; replace [|ih|] with [|j|]; auto with zarith. + 2: assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith). + 2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. + case (Zle_or_lt (2^(Z_of_nat size -1)) [|j|]); intros Hjj. + case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0. + 2: rewrite <-not_true_iff_false, ltb_spec, div2_phi in Heq0. + 2: split; auto; apply sqrt_test_true; auto with zarith. + rewrite -> ltb_spec, div2_phi in Heq0. + match goal with |- context[rec _ _ ?X] => + set (u := X) + end. + assert (H: [|u|] = ([|j|] + ([||WW ih il||])/([|j|]))/2). + unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j))); + case addc;unfold interp_carry;rewrite div2_phi;simpl zn2z_to_Z. + intros i H;rewrite lsr_spec, H;trivial. + intros i H;rewrite <- H. + case (to_Z_bounded i); intros H1i H2i. + rewrite -> add_spec, Zmod_small, lsr_spec. + change (1 * wB) with ([|(1 << (digits -1))|] * 2)%Z. + rewrite Z_div_plus_full_l; auto with zarith. + change wB with (2 * (wB/2))%Z; auto. + replace [|(1 << (digits - 1))|] with (wB/2); auto. + rewrite lsr_spec; auto. + replace (2^[|1|]) with 2%Z; auto. + split; auto with zarith. + assert ([|i|]/2 < wB/2); auto with zarith. + apply Zdiv_lt_upper_bound; auto with zarith. + apply Hrec; rewrite H; clear u H. + assert (Hf1: 0 <= [||WW ih il||]/ [|j|]) by (apply Z_div_pos; auto with zarith). + case (Zle_lt_or_eq 1 ([|j|])); auto with zarith; intros Hf2. + 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith. + split. + replace ([|j|] + [||WW ih il||]/ [|j|])%Z with + (1 * 2 + (([|j|] - 2) + [||WW ih il||] / [|j|])) by lia. + rewrite Z_div_plus_full_l; auto with zarith. + assert (0 <= ([|j|] - 2 + [||WW ih il||] / [|j|]) / 2) ; auto with zarith. + apply sqrt_test_false; auto with zarith. + apply sqrt_main; auto with zarith. + contradict Hij; apply Zle_not_lt. + assert ((1 + [|j|]) <= 2 ^ (Z_of_nat size - 1)); auto with zarith. + apply Z.le_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith. + assert (0 <= 1 + [|j|]); auto with zarith. + apply Zmult_le_compat; auto with zarith. + change ((2 ^ (Z_of_nat size - 1))^2) with (2 ^ (Z_of_nat size - 2) * wB). + apply Z.le_trans with ([|ih|] * wB); auto with zarith. + unfold zn2z_to_Z, wB; auto with zarith. +Qed. + +Lemma iter2_sqrt_correct n rec ih il j: + 2^(Z_of_nat (size - 2)) <= [|ih|] -> 0 < [|j|] -> [||WW ih il||] < ([|j|] + 1) ^ 2 -> + (forall j1, 0 < [|j1|] -> 2^(Z_of_nat n) + [|j1|] <= [|j|] -> + [||WW ih il||] < ([|j1|] + 1) ^ 2 -> + [|rec ih il j1|] ^ 2 <= [||WW ih il||] < ([|rec ih il j1|] + 1) ^ 2) -> + [|iter2_sqrt n rec ih il j|] ^ 2 <= [||WW ih il||] + < ([|iter2_sqrt n rec ih il j|] + 1) ^ 2. +Proof. + revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n. + intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct; auto with zarith. + intros; apply Hrec; auto with zarith. + rewrite Zpower_0_r; auto with zarith. + intros n Hrec rec ih il j Hi Hj Hij HHrec. + apply sqrt2_step_correct; auto. + intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. + intros j2 Hj2 H2j2 Hjp2; apply Hrec; auto with zarith. + intros j3 Hj3 Hpj3. + apply HHrec; auto. + rewrite -> inj_S, Z.pow_succ_r. + apply Z.le_trans with (2 ^Z_of_nat n + [|j2|])%Z; auto with zarith. + apply Zle_0_nat. +Qed. + +Lemma sqrt2_spec : forall x y, + wB/ 4 <= [|x|] -> + let (s,r) := sqrt2 x y in + [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ + [+|r|] <= 2 * [|s|]. + Proof. + intros ih il Hih; unfold sqrt2. + change [||WW ih il||] with ([||WW ih il||]). + assert (Hbin: forall s, s * s + 2* s + 1 = (s + 1) ^ 2) by + (intros s; ring). + assert (Hb: 0 <= wB) by (red; intros HH; discriminate). + assert (Hi2: [||WW ih il ||] < ([|max_int|] + 1) ^ 2). + apply Z.le_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith. + 2: apply refl_equal. + case (to_Z_bounded ih); case (to_Z_bounded il); intros H1 H2 H3 H4. + unfold zn2z_to_Z; auto with zarith. + case (iter2_sqrt_correct size (fun _ _ j => j) ih il max_int); auto with zarith. + apply refl_equal. + intros j1 _ HH; contradict HH. + apply Zlt_not_le. + case (to_Z_bounded j1); auto with zarith. + change (2 ^ Z_of_nat size) with ([|max_int|]+1)%Z; auto with zarith. + set (s := iter2_sqrt size (fun _ _ j : int=> j) ih il max_int). + intros Hs1 Hs2. + generalize (mulc_spec s s); case mulc. + simpl fst; simpl snd; intros ih1 il1 Hihl1. + generalize (subc_spec il il1). + case subc; intros il2 Hil2. + simpl interp_carry in Hil2. + case_eq (ih1 < ih)%int63; [idtac | rewrite <- not_true_iff_false]; + rewrite ltb_spec; intros Heq. + unfold interp_carry; rewrite Zmult_1_l. + rewrite -> Z.pow_2_r, Hihl1, Hil2. + case (Zle_lt_or_eq ([|ih1|] + 1) ([|ih|])); auto with zarith. + intros H2; contradict Hs2; apply Zle_not_lt. + replace (([|s|] + 1) ^ 2) with ([||WW ih1 il1||] + 2 * [|s|] + 1). + unfold zn2z_to_Z. + case (to_Z_bounded il); intros Hpil _. + assert (Hl1l: [|il1|] <= [|il|]). + case (to_Z_bounded il2); rewrite Hil2; auto with zarith. + assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB); auto with zarith. + case (to_Z_bounded s); intros _ Hps. + case (to_Z_bounded ih1); intros Hpih1 _; auto with zarith. + apply Z.le_trans with (([|ih1|] + 2) * wB); auto with zarith. + rewrite Zmult_plus_distr_l. + assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. + unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. + intros H2; split. + unfold zn2z_to_Z; rewrite <- H2; ring. + replace (wB + ([|il|] - [|il1|])) with ([||WW ih il||] - ([|s|] * [|s|])). + rewrite <-Hbin in Hs2; auto with zarith. + rewrite Hihl1; unfold zn2z_to_Z; rewrite <- H2; ring. + unfold interp_carry. + case (Zle_lt_or_eq [|ih|] [|ih1|]); auto with zarith; intros H. + contradict Hs1. + apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. + unfold zn2z_to_Z. + case (to_Z_bounded il); intros _ H2. + apply Z.lt_le_trans with (([|ih|] + 1) * wB + 0). + rewrite Zmult_plus_distr_l, Zplus_0_r; auto with zarith. + case (to_Z_bounded il1); intros H3 _. + apply Zplus_le_compat; auto with zarith. + split. + rewrite Z.pow_2_r, Hihl1. + unfold zn2z_to_Z; ring[Hil2 H]. + replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]). + unfold zn2z_to_Z at 2; rewrite <-Hihl1. + rewrite <-Hbin in Hs2; auto with zarith. + unfold zn2z_to_Z; rewrite H, Hil2; ring. + unfold interp_carry in Hil2 |- *. + assert (Hsih: [|ih - 1|] = [|ih|] - 1). + rewrite sub_spec, Zmod_small; auto; replace [|1|] with 1; auto. + case (to_Z_bounded ih); intros H1 H2. + split; auto with zarith. + apply Z.le_trans with (wB/4 - 1); auto with zarith. + case_eq (ih1 < ih - 1)%int63; [idtac | rewrite <- not_true_iff_false]; + rewrite ltb_spec, Hsih; intros Heq. + rewrite Z.pow_2_r, Hihl1. + case (Zle_lt_or_eq ([|ih1|] + 2) [|ih|]); auto with zarith. + intros H2; contradict Hs2; apply Zle_not_lt. + replace (([|s|] + 1) ^ 2) with ([||WW ih1 il1||] + 2 * [|s|] + 1). + unfold zn2z_to_Z. + assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB + ([|il|] - [|il1|])); + auto with zarith. + rewrite <-Hil2. + case (to_Z_bounded il2); intros Hpil2 _. + apply Z.le_trans with ([|ih|] * wB + - wB); auto with zarith. + case (to_Z_bounded s); intros _ Hps. + assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. + apply Z.le_trans with ([|ih1|] * wB + 2 * wB); auto with zarith. + assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB); auto with zarith. + rewrite Zmult_plus_distr_l in Hi; auto with zarith. + unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. + intros H2; unfold zn2z_to_Z; rewrite <-H2. + split. + replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + rewrite <-Hil2; ring. + replace (1 * wB + [|il2|]) with ([||WW ih il||] - [||WW ih1 il1||]). + unfold zn2z_to_Z at 2; rewrite <-Hihl1. + rewrite <-Hbin in Hs2; auto with zarith. + unfold zn2z_to_Z; rewrite <-H2. + replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + rewrite <-Hil2; ring. + case (Zle_lt_or_eq ([|ih|] - 1) ([|ih1|])); auto with zarith; intros H1. + assert (He: [|ih|] = [|ih1|]). + apply Zle_antisym; auto with zarith. + case (Zle_or_lt [|ih1|] [|ih|]); auto; intros H2. + contradict Hs1; apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. + unfold zn2z_to_Z. + case (to_Z_bounded il); intros _ Hpil1. + apply Z.lt_le_trans with (([|ih|] + 1) * wB). + rewrite Zmult_plus_distr_l, Zmult_1_l; auto with zarith. + case (to_Z_bounded il1); intros Hpil2 _. + apply Z.le_trans with (([|ih1|]) * wB); auto with zarith. + contradict Hs1; apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. + unfold zn2z_to_Z; rewrite He. + assert ([|il|] - [|il1|] < 0); auto with zarith. + rewrite <-Hil2. + case (to_Z_bounded il2); auto with zarith. + split. + rewrite Z.pow_2_r, Hihl1. + unfold zn2z_to_Z; rewrite <-H1. + apply trans_equal with ([|ih|] * wB + [|il1|] + ([|il|] - [|il1|])). + ring. + rewrite <-Hil2; ring. + replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]). + unfold zn2z_to_Z at 2; rewrite <- Hihl1. + rewrite <-Hbin in Hs2; auto with zarith. + unfold zn2z_to_Z. + rewrite <-H1. + ring_simplify. + apply trans_equal with (wB + ([|il|] - [|il1|])). + ring. + rewrite <-Hil2; ring. +Qed. + +(* of_pos *) +Lemma of_pos_rec_spec (k: nat) : + (k <= size)%nat → + ∀ p, φ(of_pos_rec k p) = Zpos p mod 2 ^ Z.of_nat k. +Proof. + elim k; clear k. + intros _ p; simpl; rewrite to_Z_0, Zmod_1_r; reflexivity. + intros n ih hn. + assert (n <= size)%nat as hn' by lia. + specialize (ih hn'). + intros [ p | p | ]. + 3: { + rewrite Zmod_small. reflexivity. + split. lia. + apply Zpower_gt_1; lia. + } + - simpl. + destruct (bit_add_or (of_pos_rec n p << 1) 1) as (H1, _). + rewrite <- H1;clear H1. + 2: { + intros i; rewrite bit_lsl, bit_1. + case eqbP. + + intros h; apply to_Z_inj in h; subst. exact (λ e _, diff_false_true e). + + exact (λ _ _, diff_false_true). + } + rewrite add_spec, lsl_spec, ih, to_Z_1; clear ih. + rewrite Z.pow_pos_fold, Zpos_P_of_succ_nat. + change (Zpos p~1) with (2 ^ 1 * Zpos p + 1)%Z. + rewrite Zmod_distr by lia. + rewrite Zpower_Zsucc by auto with zarith. + rewrite Zplus_mod_idemp_l. + rewrite Zmod_small. + rewrite Zmult_mod_distr_l; lia. + set (a := Z.of_nat n). + set (b := Zpos p). + change (2 ^ 1) with 2. + pose proof (pow2_pos a (Nat2Z.is_nonneg _)). + elim_div; intros x y [ ? ha]. lia. + destruct ha as [ ha | ]. 2: lia. + split. lia. + apply Z.lt_le_trans with (2 ^ (a + 1)). + 2: apply Z.pow_le_mono_r; subst a; lia. + fold (Z.succ a); rewrite Z.pow_succ_r. lia. + subst a; lia. + - simpl. rewrite lsl_spec, ih, to_Z_1, Zmod_small. + rewrite Z.pow_pos_fold, Zpos_P_of_succ_nat, Zpower_Zsucc by lia. + change (Zpos p~0) with (2 ^ 1 * Zpos p)%Z. + rewrite Z.mul_mod_distr_l; auto with zarith. + set (a := Z.of_nat n). + set (b := Zpos p). + change (2 ^ 1) with 2. + pose proof (pow2_pos a (Nat2Z.is_nonneg _)). + elim_div; intros x y [ ? ha]. lia. + destruct ha as [ ha | ]. 2: lia. + split. lia. + apply Z.lt_le_trans with (2 ^ (a + 1)). + 2: apply Z.pow_le_mono_r; subst a; lia. + fold (Z.succ a); rewrite Z.pow_succ_r. lia. + subst a; lia. +Qed. + +Lemma is_int n : + 0 <= n < 2 ^ φ digits → + n = φ (of_Z n). +Proof. + destruct n. reflexivity. 2: lia. + intros [_ h]. simpl. + unfold of_pos. rewrite of_pos_rec_spec by lia. + symmetry; apply Z.mod_small. split. lia. exact h. +Qed. + +Lemma of_Z_spec n : [| of_Z n |] = n mod wB. +Proof. + destruct n. reflexivity. + { now simpl; unfold of_pos; rewrite of_pos_rec_spec by lia. } + simpl; unfold of_pos; rewrite opp_spec. + rewrite of_pos_rec_spec; [ |auto]; fold wB. + now rewrite <-(Z.sub_0_l), Zminus_mod_idemp_r. +Qed. + +(* General lemmas *) +Lemma negbE a b : a = negb b → negb a = b. +Proof. intros ->; apply negb_involutive. Qed. + +Lemma Z_oddE a : Z.odd a = (a mod 2 =? 1)%Z. +Proof. rewrite Zmod_odd; case Z.odd; reflexivity. Qed. + +Lemma Z_evenE a : Z.even a = (a mod 2 =? 0)%Z. +Proof. rewrite Zmod_even; case Z.even; reflexivity. Qed. + +(* is_zero *) +Lemma is_zeroE n : is_zero n = Z.eqb (φ n) 0. +Proof. + case Z.eqb_spec. + - intros h; apply (to_Z_inj n 0) in h; subst n; reflexivity. + - generalize (proj1 (is_zero_spec n)). + case is_zero; auto; intros ->; auto; destruct 1; reflexivity. +Qed. + +(* bit *) +Lemma bitE i j : bit i j = Z.testbit φ(i) φ(j). +Proof. + apply negbE; rewrite is_zeroE, lsl_spec, lsr_spec. + generalize (φ i) (to_Z_bounded i) (φ j) (to_Z_bounded j); clear i j; + intros i [hi hi'] j [hj hj']. + rewrite Z.testbit_eqb by auto; rewrite <- Z_oddE, Z.negb_odd, Z_evenE. + remember (i / 2 ^ j) as k. + change wB with (2 * 2 ^ φ (digits - 1)). + unfold Z.modulo at 2. + generalize (Z_div_mod_full k 2 (λ k, let 'eq_refl := k in I)); unfold Remainder. + destruct Z.div_eucl as [ p q ]; intros [hk [ hq | ]]. 2: lia. + rewrite hk. + remember φ (digits - 1) as m. + replace ((_ + _) * _) with (q * 2 ^ m + p * (2 * 2 ^ m)) by ring. + rewrite Z_mod_plus by (subst m; reflexivity). + assert (q = 0 ∨ q = 1) as D by lia. + destruct D; subst; reflexivity. +Qed. + +(* land, lor, lxor *) +Lemma lt_pow_lt_log d k n : + 0 < d <= n → + 0 <= k < 2 ^ d → + Z.log2 k < n. +Proof. + intros [hd hdn] [hk hkd]. + assert (k = 0 ∨ 0 < k) as D by lia. + clear hk; destruct D as [ hk | hk ]. + - subst k; simpl; lia. + - apply Z.log2_lt_pow2. lia. + eapply Z.lt_le_trans. eassumption. + apply Z.pow_le_mono_r; lia. +Qed. + +Lemma land_spec' x y : φ (x land y) = Z.land φ(x) φ(y). +Proof. + apply Z.bits_inj'; intros n hn. + destruct (to_Z_bounded (x land y)) as [ hxy hxy' ]. + destruct (to_Z_bounded x) as [ hx hx' ]. + destruct (to_Z_bounded y) as [ hy hy' ]. + case (Z_lt_le_dec n (φ digits)); intros hd. + 2: { + rewrite !Z.bits_above_log2; auto. + - apply Z.land_nonneg; auto. + - eapply Z.le_lt_trans. + apply Z.log2_land; assumption. + apply Z.min_lt_iff. + left. apply (lt_pow_lt_log φ digits). exact (conj eq_refl hd). + split; assumption. + - apply (lt_pow_lt_log φ digits). exact (conj eq_refl hd). + split; assumption. + } + rewrite (is_int n). + rewrite Z.land_spec, <- !bitE, land_spec; reflexivity. + apply (conj hn). + apply (Z.lt_trans _ _ _ hd). + apply Zpower2_lt_lin. lia. +Qed. + +Lemma lor_spec' x y : φ (x lor y) = Z.lor φ(x) φ(y). +Proof. + apply Z.bits_inj'; intros n hn. + destruct (to_Z_bounded (x lor y)) as [ hxy hxy' ]. + destruct (to_Z_bounded x) as [ hx hx' ]. + destruct (to_Z_bounded y) as [ hy hy' ]. + case (Z_lt_le_dec n (φ digits)); intros hd. + 2: { + rewrite !Z.bits_above_log2; auto. + - apply Z.lor_nonneg; auto. + - rewrite Z.log2_lor by assumption. + apply Z.max_lub_lt; apply (lt_pow_lt_log φ digits); split; assumption || reflexivity. + - apply (lt_pow_lt_log φ digits); split; assumption || reflexivity. + } + rewrite (is_int n). + rewrite Z.lor_spec, <- !bitE, lor_spec; reflexivity. + apply (conj hn). + apply (Z.lt_trans _ _ _ hd). + apply Zpower2_lt_lin. lia. +Qed. + +Lemma lxor_spec' x y : φ (x lxor y) = Z.lxor φ(x) φ(y). +Proof. + apply Z.bits_inj'; intros n hn. + destruct (to_Z_bounded (x lxor y)) as [ hxy hxy' ]. + destruct (to_Z_bounded x) as [ hx hx' ]. + destruct (to_Z_bounded y) as [ hy hy' ]. + case (Z_lt_le_dec n (φ digits)); intros hd. + 2: { + rewrite !Z.bits_above_log2; auto. + - apply Z.lxor_nonneg; split; auto. + - eapply Z.le_lt_trans. + apply Z.log2_lxor; assumption. + apply Z.max_lub_lt; apply (lt_pow_lt_log φ digits); split; assumption || reflexivity. + - apply (lt_pow_lt_log φ digits); split; assumption || reflexivity. + } + rewrite (is_int n). + rewrite Z.lxor_spec, <- !bitE, lxor_spec; reflexivity. + apply (conj hn). + apply (Z.lt_trans _ _ _ hd). + apply Zpower2_lt_lin. lia. +Qed. + +Lemma landC i j : i land j = j land i. +Proof. + apply bit_ext; intros n. + rewrite !land_spec, andb_comm; auto. +Qed. + +Lemma landA i j k : i land (j land k) = i land j land k. +Proof. + apply bit_ext; intros n. + rewrite !land_spec, andb_assoc; auto. +Qed. + +Lemma land0 i : 0 land i = 0%int63. +Proof. + apply bit_ext; intros n. + rewrite land_spec, bit_0; auto. +Qed. + +Lemma land0_r i : i land 0 = 0%int63. +Proof. rewrite landC; exact (land0 i). Qed. + +Lemma lorC i j : i lor j = j lor i. +Proof. + apply bit_ext; intros n. + rewrite !lor_spec, orb_comm; auto. +Qed. + +Lemma lorA i j k : i lor (j lor k) = i lor j lor k. +Proof. + apply bit_ext; intros n. + rewrite !lor_spec, orb_assoc; auto. +Qed. + +Lemma lor0 i : 0 lor i = i. +Proof. + apply bit_ext; intros n. + rewrite lor_spec, bit_0; auto. +Qed. + +Lemma lor0_r i : i lor 0 = i. +Proof. rewrite lorC; exact (lor0 i). Qed. + +Lemma lxorC i j : i lxor j = j lxor i. +Proof. + apply bit_ext; intros n. + rewrite !lxor_spec, xorb_comm; auto. +Qed. + +Lemma lxorA i j k : i lxor (j lxor k) = i lxor j lxor k. +Proof. + apply bit_ext; intros n. + rewrite !lxor_spec, xorb_assoc; auto. +Qed. + +Lemma lxor0 i : 0 lxor i = i. +Proof. + apply bit_ext; intros n. + rewrite lxor_spec, bit_0, xorb_false_l; auto. +Qed. + +Lemma lxor0_r i : i lxor 0 = i. +Proof. rewrite lxorC; exact (lxor0 i). Qed. diff --git a/theories/Numbers/Cyclic/Int63/Ring63.v b/theories/Numbers/Cyclic/Int63/Ring63.v new file mode 100644 index 0000000000..d230435378 --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Ring63.v @@ -0,0 +1,65 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Int63 numbers defines Z/(2^63)Z, and can hence be equipped + with a ring structure and a ring tactic *) + +Require Import Cyclic63 CyclicAxioms. + +Local Open Scope int63_scope. + +(** Detection of constants *) + +Ltac isInt63cst t := + match eval lazy delta [add] in (t + 1)%int63 with + | add _ _ => constr:(false) + | _ => constr:(true) + end. + +Ltac Int63cst t := + match eval lazy delta [add] in (t + 1)%int63 with + | add _ _ => constr:(NotConstant) + | _ => constr:(t) + end. + +(** The generic ring structure inferred from the Cyclic structure *) + +Module Int63ring := CyclicRing Int63Cyclic. + +(** Unlike in the generic [CyclicRing], we can use Leibniz here. *) + +Lemma Int63_canonic : forall x y, to_Z x = to_Z y -> x = y. +Proof to_Z_inj. + +Lemma ring_theory_switch_eq : + forall A (R R':A->A->Prop) zero one add mul sub opp, + (forall x y : A, R x y -> R' x y) -> + ring_theory zero one add mul sub opp R -> + ring_theory zero one add mul sub opp R'. +Proof. +intros A R R' zero one add mul sub opp Impl Ring. +constructor; intros; apply Impl; apply Ring. +Qed. + +Lemma Int63Ring : ring_theory 0 1 add mul sub opp Logic.eq. +Proof. +exact (ring_theory_switch_eq _ _ _ _ _ _ _ _ _ Int63_canonic Int63ring.CyclicRing). +Qed. + +Lemma eq31_correct : forall x y, eqb x y = true -> x=y. +Proof. now apply eqb_spec. Qed. + +Add Ring Int63Ring : Int63Ring + (decidable eq31_correct, + constants [Int63cst]). + +Section TestRing. +Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x. +intros. ring. +Qed. +End TestRing. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index bc366c508d..9fcb029b3c 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -22,14 +22,16 @@ Ltac nzsimpl' := autorewrite with nz nz'. Theorem add_0_r : forall n, n + 0 == n. Proof. -nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_succ_r : forall n m, n + S m == S (n + m). Proof. -intros n m; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + intros n m; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_succ_comm : forall n m, S n + m == n + S m. @@ -41,8 +43,9 @@ Hint Rewrite add_0_r add_succ_r : nz. Theorem add_comm : forall n m, n + m == m + n. Proof. -intros n m; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + intros n m; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_1_l : forall n, 1 + n == S n. @@ -59,14 +62,16 @@ Hint Rewrite add_1_l add_1_r : nz. Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. -intros n m p; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite succ_inj_wd. + intros n m p; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_cancel_l : forall n m p, p + n == p + m <-> n == m. Proof. -intros n m p; nzinduct p. now nzsimpl. -intro p. nzsimpl. now rewrite succ_inj_wd. +intros n m p; nzinduct p. +- now nzsimpl. +- intro p. nzsimpl. now rewrite succ_inj_wd. Qed. Theorem add_cancel_r : forall n m p, n + p == m + p <-> n == m. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 99812ee3fe..5f102e853b 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -17,8 +17,8 @@ Include NZBaseProp NZ <+ NZMulProp NZ <+ NZOrderProp NZ. Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m. Proof. -intros n m p; nzinduct p. now nzsimpl. -intro p. nzsimpl. now rewrite <- succ_lt_mono. + intros n m p; nzinduct p. - now nzsimpl. + - intro p. nzsimpl. now rewrite <- succ_lt_mono. Qed. Theorem add_lt_mono_r : forall n m p, n < m <-> n + p < m + p. @@ -35,8 +35,8 @@ Qed. Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m. Proof. -intros n m p; nzinduct p. now nzsimpl. -intro p. nzsimpl. now rewrite <- succ_le_mono. + intros n m p; nzinduct p. - now nzsimpl. + - intro p. nzsimpl. now rewrite <- succ_le_mono. Qed. Theorem add_le_mono_r : forall n m p, n <= m <-> n + p <= m + p. @@ -124,9 +124,9 @@ Qed. Theorem add_le_cases : forall n m p q, n + m <= p + q -> n <= p \/ m <= q. Proof. intros n m p q H. -destruct (le_gt_cases n p) as [H1 | H1]. now left. -destruct (le_gt_cases m q) as [H2 | H2]. now right. -contradict H; rewrite nle_gt. now apply add_lt_mono. +destruct (le_gt_cases n p) as [H1 | H1]. - now left. +- destruct (le_gt_cases m q) as [H2 | H2]. + now right. + + contradict H; rewrite nle_gt. now apply add_lt_mono. Qed. Theorem add_neg_cases : forall n m, n + m < 0 -> n < 0 \/ m < 0. @@ -156,10 +156,10 @@ Qed. Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p. Proof. - intros n m H. apply le_ind with (4:=H). solve_proper. - exists 0; nzsimpl; split; order. - clear m H. intros m H (p & EQ & LE). exists (S p). - split. nzsimpl. now f_equiv. now apply le_le_succ_r. + intros n m H. apply le_ind with (4:=H). - solve_proper. + - exists 0; nzsimpl; split; order. + - clear m H. intros m H (p & EQ & LE). exists (S p). + split. + nzsimpl. now f_equiv. + now apply le_le_succ_r. Qed. (** For the moment, it doesn't seem possible to relate diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 595b2182ab..840a798d9b 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -49,8 +49,8 @@ bidirectional induction steps *) Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2. Proof. intros; split. -apply succ_inj. -intros. now f_equiv. +- apply succ_inj. +- intros. now f_equiv. Qed. Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m. @@ -72,9 +72,9 @@ Theorem central_induction : forall n, A n. Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. -solve_proper. -intro; now apply bi_induction. -intro; pose proof (Step n); tauto. +- solve_proper. +- intro; now apply bi_induction. +- intro; pose proof (Step n); tauto. Qed. End CentralInduction. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 550aa226ac..b94cef7cee 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -54,22 +54,22 @@ Proof. intros b. assert (U : forall q1 q2 r1 r2, b*q1+r1 == b*q2+r2 -> 0<=r1<b -> 0<=r2 -> q1<q2 -> False). - intros q1 q2 r1 r2 EQ LT Hr1 Hr2. - contradict EQ. - apply lt_neq. - apply lt_le_trans with (b*q1+b). - rewrite <- add_lt_mono_l. tauto. - apply le_trans with (b*q2). - rewrite mul_comm, <- mul_succ_l, mul_comm. - apply mul_le_mono_nonneg_l; intuition; try order. - rewrite le_succ_l; auto. - rewrite <- (add_0_r (b*q2)) at 1. - rewrite <- add_le_mono_l. tauto. - -intros q1 q2 r1 r2 Hr1 Hr2 EQ; destruct (lt_trichotomy q1 q2) as [LT|[EQ'|GT]]. -elim (U q1 q2 r1 r2); intuition. -split; auto. rewrite EQ' in EQ. rewrite add_cancel_l in EQ; auto. -elim (U q2 q1 r2 r1); intuition. +- intros q1 q2 r1 r2 EQ LT Hr1 Hr2. + contradict EQ. + apply lt_neq. + apply lt_le_trans with (b*q1+b). + + rewrite <- add_lt_mono_l. tauto. + + apply le_trans with (b*q2). + * rewrite mul_comm, <- mul_succ_l, mul_comm. + apply mul_le_mono_nonneg_l; intuition; try order. + rewrite le_succ_l; auto. + * rewrite <- (add_0_r (b*q2)) at 1. + rewrite <- add_le_mono_l. tauto. + +- intros q1 q2 r1 r2 Hr1 Hr2 EQ; destruct (lt_trichotomy q1 q2) as [LT|[EQ'|GT]]. + + elim (U q1 q2 r1 r2); intuition. + + split; auto. rewrite EQ' in EQ. rewrite add_cancel_l in EQ; auto. + + elim (U q2 q1 r2 r1); intuition. Qed. Theorem div_unique: @@ -78,8 +78,8 @@ Theorem div_unique: Proof. intros a b q r Ha (Hb,Hr) EQ. destruct (div_mod_unique b q (a/b) r (a mod b)); auto. -apply mod_bound_pos; order. -rewrite <- div_mod; order. +- apply mod_bound_pos; order. +- rewrite <- div_mod; order. Qed. Theorem mod_unique: @@ -88,8 +88,8 @@ Theorem mod_unique: Proof. intros a b q r Ha (Hb,Hr) EQ. destruct (div_mod_unique b q (a/b) r (a mod b)); auto. -apply mod_bound_pos; order. -rewrite <- div_mod; order. +- apply mod_bound_pos; order. +- rewrite <- div_mod; order. Qed. Theorem div_unique_exact a b q: @@ -167,16 +167,16 @@ Qed. Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a. Proof. intros; symmetry. apply div_unique_exact; trivial. -apply mul_nonneg_nonneg; order. -apply mul_comm. +- apply mul_nonneg_nonneg; order. +- apply mul_comm. Qed. Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0. Proof. intros; symmetry. apply mod_unique with a; try split; try order. -apply mul_nonneg_nonneg; order. -nzsimpl; apply mul_comm. +- apply mul_nonneg_nonneg; order. +- nzsimpl; apply mul_comm. Qed. @@ -187,10 +187,10 @@ Qed. Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. Proof. intros. destruct (le_gt_cases b a). -apply le_trans with b; auto. -apply lt_le_incl. destruct (mod_bound_pos a b); auto. -rewrite lt_eq_cases; right. -apply mod_small; auto. +- apply le_trans with b; auto. + apply lt_le_incl. destruct (mod_bound_pos a b); auto. +- rewrite lt_eq_cases; right. + apply mod_small; auto. Qed. @@ -219,9 +219,9 @@ Qed. Lemma div_small_iff : forall a b, 0<=a -> 0<b -> (a/b==0 <-> a<b). Proof. intros a b Ha Hb; split; intros Hab. -destruct (lt_ge_cases a b); auto. -symmetry in Hab. contradict Hab. apply lt_neq, div_str_pos; auto. -apply div_small; auto. +- destruct (lt_ge_cases a b); auto. + symmetry in Hab. contradict Hab. apply lt_neq, div_str_pos; auto. +- apply div_small; auto. Qed. Lemma mod_small_iff : forall a b, 0<=a -> 0<b -> (a mod b == a <-> a<b). @@ -236,9 +236,9 @@ Qed. Lemma div_str_pos_iff : forall a b, 0<=a -> 0<b -> (0<a/b <-> b<=a). Proof. intros a b Ha Hb; split; intros Hab. -destruct (lt_ge_cases a b) as [LT|LE]; auto. -rewrite <- div_small_iff in LT; order. -apply div_str_pos; auto. +- destruct (lt_ge_cases a b) as [LT|LE]; auto. + rewrite <- div_small_iff in LT; order. +- apply div_str_pos; auto. Qed. @@ -250,14 +250,14 @@ Proof. intros. assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1). destruct (lt_ge_cases a b). -rewrite div_small; try split; order. -rewrite (div_mod a b) at 2 by order. -apply lt_le_trans with (b*(a/b)). -rewrite <- (mul_1_l (a/b)) at 1. -rewrite <- mul_lt_mono_pos_r; auto. -apply div_str_pos; auto. -rewrite <- (add_0_r (b*(a/b))) at 1. -rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. +- rewrite div_small; try split; order. +- rewrite (div_mod a b) at 2 by order. + apply lt_le_trans with (b*(a/b)). + + rewrite <- (mul_1_l (a/b)) at 1. + rewrite <- mul_lt_mono_pos_r; auto. + apply div_str_pos; auto. + + rewrite <- (add_0_r (b*(a/b))) at 1. + rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed. (** [le] is compatible with a positive division. *) @@ -276,8 +276,8 @@ apply lt_le_trans with b; auto. rewrite (div_mod b c) at 1 by order. rewrite <- add_assoc, <- add_le_mono_l. apply le_trans with (c+0). -nzsimpl; destruct (mod_bound_pos b c); order. -rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order. +- nzsimpl; destruct (mod_bound_pos b c); order. +- rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order. Qed. (** The following two properties could be used as specification of div *) @@ -334,11 +334,11 @@ Theorem div_le_lower_bound: Proof. intros a b q Ha Hb H. destruct (lt_ge_cases 0 q). -rewrite <- (div_mul q b); try order. -apply div_le_mono; auto. -rewrite mul_comm; split; auto. -apply lt_le_incl, mul_pos_pos; auto. -apply le_trans with 0; auto; apply div_pos; auto. +- rewrite <- (div_mul q b); try order. + apply div_le_mono; auto. + rewrite mul_comm; split; auto. + apply lt_le_incl, mul_pos_pos; auto. +- apply le_trans with 0; auto; apply div_pos; auto. Qed. (** A division respects opposite monotonicity for the divisor *) @@ -350,10 +350,10 @@ Proof. apply div_le_lower_bound; auto. rewrite (div_mod p r) at 2 by order. apply le_trans with (r*(p/r)). - apply mul_le_mono_nonneg_r; try order. - apply div_pos; order. - rewrite <- (add_0_r (r*(p/r))) at 1. - rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order. + - apply mul_le_mono_nonneg_r; try order. + apply div_pos; order. + - rewrite <- (add_0_r (r*(p/r))) at 1. + rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order. Qed. @@ -365,9 +365,9 @@ Proof. intros. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound_pos; auto. - rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. - now rewrite mul_comm. + - apply mod_bound_pos; auto. + - rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. + now rewrite mul_comm. Qed. Lemma div_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> @@ -396,14 +396,14 @@ Proof. intros. symmetry. apply div_unique with ((a mod b)*c). - apply mul_nonneg_nonneg; order. - split. - apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order. - rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto. - rewrite (div_mod a b) at 1 by order. - rewrite mul_add_distr_r. - rewrite add_cancel_r. - rewrite <- 2 mul_assoc. now rewrite (mul_comm c). + - apply mul_nonneg_nonneg; order. + - split. + + apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order. + + rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto. + - rewrite (div_mod a b) at 1 by order. + rewrite mul_add_distr_r. + rewrite add_cancel_r. + rewrite <- 2 mul_assoc. now rewrite (mul_comm c). Qed. Lemma div_mul_cancel_l : forall a b c, 0<=a -> 0<b -> 0<c -> @@ -418,10 +418,10 @@ Proof. intros. rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))). rewrite <- div_mod. - rewrite div_mul_cancel_l; auto. - rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. - apply div_mod; order. - rewrite <- neq_mul_0; intuition; order. + - rewrite div_mul_cancel_l; auto. + rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. + apply div_mod; order. + - rewrite <- neq_mul_0; intuition; order. Qed. Lemma mul_mod_distr_r: forall a b c, 0<=a -> 0<b -> 0<c -> @@ -447,8 +447,8 @@ Proof. rewrite add_comm, (mul_comm n), (mul_comm _ b). rewrite mul_add_distr_l, mul_assoc. intros. rewrite mod_add; auto. - now rewrite mul_comm. - apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto. + - now rewrite mul_comm. + - apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto. Qed. Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -460,8 +460,8 @@ Qed. Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n. Proof. - intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity. - now destruct (mod_bound_pos b n). + intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity. + - now destruct (mod_bound_pos b n). Qed. Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -471,8 +471,8 @@ Proof. generalize (add_nonneg_nonneg _ _ Ha Hb). rewrite (div_mod a n) at 1 2 by order. rewrite <- add_assoc, add_comm, mul_comm. - intros. rewrite mod_add; trivial. reflexivity. - apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto. + intros. rewrite mod_add; trivial. - reflexivity. + - apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto. Qed. Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -484,8 +484,8 @@ Qed. Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. - intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity. - now destruct (mod_bound_pos b n). + intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity. + - now destruct (mod_bound_pos b n). Qed. Lemma div_div : forall a b c, 0<=a -> 0<b -> 0<c -> @@ -494,18 +494,18 @@ Proof. intros a b c Ha Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b); trivial. (* begin 0<= ... <b*c *) - destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos. - split. - apply add_nonneg_nonneg; auto. - apply mul_nonneg_nonneg; order. - apply lt_le_trans with (b*((a/b) mod c) + b). - rewrite <- add_lt_mono_l; auto. - rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto. - (* end 0<= ... < b*c *) - rewrite (div_mod a b) at 1 by order. - rewrite add_assoc, add_cancel_r. - rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. - apply div_mod; order. + - destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos. + split. + + apply add_nonneg_nonneg; auto. + apply mul_nonneg_nonneg; order. + + apply lt_le_trans with (b*((a/b) mod c) + b). + * rewrite <- add_lt_mono_l; auto. + * rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto. + (* end 0<= ... < b*c *) + - rewrite (div_mod a b) at 1 by order. + rewrite add_assoc, add_cancel_r. + rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. + apply div_mod; order. Qed. Lemma mod_mul_r : forall a b c, 0<=a -> 0<b -> 0<c -> @@ -527,10 +527,10 @@ Theorem div_mul_le: Proof. intros. apply div_le_lower_bound; auto. - apply mul_nonneg_nonneg; auto. - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. - apply mul_le_mono_nonneg_l; auto. - apply mul_div_le; auto. + - apply mul_nonneg_nonneg; auto. + - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. + apply mul_le_mono_nonneg_l; auto. + apply mul_div_le; auto. Qed. (** mod is related to divisibility *) @@ -539,9 +539,9 @@ Lemma mod_divides : forall a b, 0<=a -> 0<b -> (a mod b == 0 <-> exists c, a == b*c). Proof. split. - intros. exists (a/b). rewrite div_exact; auto. - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. - rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. + - intros. exists (a/b). rewrite div_exact; auto. + - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. + rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. Qed. End NZDivProp. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index c38d1aac31..1ac89ce942 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -72,15 +72,15 @@ Lemma eq_mul_1_nonneg : forall n m, Proof. intros n m Hn H. le_elim Hn. - destruct (lt_ge_cases m 0) as [Hm|Hm]. - generalize (mul_pos_neg n m Hn Hm). order'. - le_elim Hm. - apply le_succ_l in Hn. rewrite <- one_succ in Hn. - le_elim Hn. - generalize (lt_1_mul_pos n m Hn Hm). order. - rewrite <- Hn, mul_1_l in H. now split. - rewrite <- Hm, mul_0_r in H. order'. - rewrite <- Hn, mul_0_l in H. order'. + - destruct (lt_ge_cases m 0) as [Hm|Hm]. + + generalize (mul_pos_neg n m Hn Hm). order'. + + le_elim Hm. + * apply le_succ_l in Hn. rewrite <- one_succ in Hn. + le_elim Hn. + -- generalize (lt_1_mul_pos n m Hn Hm). order. + -- rewrite <- Hn, mul_1_l in H. now split. + * rewrite <- Hm, mul_0_r in H. order'. + - rewrite <- Hn, mul_0_l in H. order'. Qed. Lemma eq_mul_1_nonneg' : forall n m, @@ -117,13 +117,13 @@ Lemma divide_antisym_nonneg : forall n m, Proof. intros n m Hn Hm (q,Hq) (r,Hr). le_elim Hn. - destruct (lt_ge_cases q 0) as [Hq'|Hq']. - generalize (mul_neg_pos q n Hq' Hn). order. - rewrite Hq, mul_assoc in Hr. symmetry in Hr. - apply mul_id_l in Hr; [|order]. - destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial. - now rewrite H, mul_1_l in Hq. - rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn. + - destruct (lt_ge_cases q 0) as [Hq'|Hq']. + + generalize (mul_neg_pos q n Hq' Hn). order. + + rewrite Hq, mul_assoc in Hr. symmetry in Hr. + apply mul_id_l in Hr; [|order]. + destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial. + now rewrite H, mul_1_l in Hq. + - rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn. Qed. Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m). @@ -140,8 +140,8 @@ Lemma mul_divide_cancel_l : forall n m p, p ~= 0 -> ((p * n | p * m) <-> (n | m)). Proof. intros n m p Hp. split. - intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq. - apply mul_divide_mono_l. + - intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq. + - apply mul_divide_mono_l. Qed. Lemma mul_divide_cancel_r : forall n m p, p ~= 0 -> @@ -179,14 +179,14 @@ Qed. Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m. Proof. intros n m Hm (q,Hq). - destruct (le_gt_cases n 0) as [Hn|Hn]. order. - rewrite Hq. - destruct (lt_ge_cases q 0) as [Hq'|Hq']. - generalize (mul_neg_pos q n Hq' Hn). order. - le_elim Hq'. - rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial. - now rewrite one_succ, le_succ_l. - rewrite <- Hq', mul_0_l in Hq. order. + destruct (le_gt_cases n 0) as [Hn|Hn]. - order. + - rewrite Hq. + destruct (lt_ge_cases q 0) as [Hq'|Hq']. + + generalize (mul_neg_pos q n Hq' Hn). order. + + le_elim Hq'. + * rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial. + now rewrite one_succ, le_succ_l. + * rewrite <- Hq', mul_0_l in Hq. order. Qed. (** Basic properties of gcd *) @@ -197,28 +197,28 @@ Lemma gcd_unique : forall n m p, gcd n m == p. Proof. intros n m p Hp Hn Hm H. - apply divide_antisym_nonneg; trivial. apply gcd_nonneg. - apply H. apply gcd_divide_l. apply gcd_divide_r. - now apply gcd_greatest. + apply divide_antisym_nonneg; trivial. - apply gcd_nonneg. + - apply H. + apply gcd_divide_l. + apply gcd_divide_r. + - now apply gcd_greatest. Qed. Instance gcd_wd : Proper (eq==>eq==>eq) gcd. Proof. intros x x' Hx y y' Hy. apply gcd_unique. - apply gcd_nonneg. - rewrite Hx. apply gcd_divide_l. - rewrite Hy. apply gcd_divide_r. - intro. rewrite Hx, Hy. apply gcd_greatest. + - apply gcd_nonneg. + - rewrite Hx. apply gcd_divide_l. + - rewrite Hy. apply gcd_divide_r. + - intro. rewrite Hx, Hy. apply gcd_greatest. Qed. Lemma gcd_divide_iff : forall n m p, (p | gcd n m) <-> (p | n) /\ (p | m). Proof. - intros. split. split. - transitivity (gcd n m); trivial using gcd_divide_l. - transitivity (gcd n m); trivial using gcd_divide_r. - intros (H,H'). now apply gcd_greatest. + intros. split. - split. + + transitivity (gcd n m); trivial using gcd_divide_l. + + transitivity (gcd n m); trivial using gcd_divide_r. + - intros (H,H'). now apply gcd_greatest. Qed. Lemma gcd_unique_alt : forall n m p, 0<=p -> @@ -227,9 +227,9 @@ Lemma gcd_unique_alt : forall n m p, 0<=p -> Proof. intros n m p Hp H. apply gcd_unique; trivial. - apply H. apply divide_refl. - apply H. apply divide_refl. - intros. apply H. now split. + - apply H. apply divide_refl. + - apply H. apply divide_refl. + - intros. apply H. now split. Qed. Lemma gcd_comm : forall n m, gcd n m == gcd m n. @@ -247,8 +247,8 @@ Qed. Lemma gcd_0_l_nonneg : forall n, 0<=n -> gcd 0 n == n. Proof. intros. apply gcd_unique; trivial. - apply divide_0_r. - apply divide_refl. + - apply divide_0_r. + - apply divide_refl. Qed. Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n. @@ -284,24 +284,26 @@ Qed. Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0. Proof. - intros. split. split. - now apply gcd_eq_0_l with m. - now apply gcd_eq_0_r with n. - intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg. + intros. split. + - split. + + now apply gcd_eq_0_l with m. + + now apply gcd_eq_0_r with n. + - intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg. Qed. Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n. Proof. intros n m Hn. apply gcd_unique_alt; trivial. - intros q. split. split; trivial. now apply divide_mul_l. - now destruct 1. + intros q. split. - split; trivial. now apply divide_mul_l. + - now destruct 1. Qed. Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n). Proof. - intros n m Hn. split. intros (q,Hq). rewrite Hq. - rewrite mul_comm. now apply gcd_mul_diag_l. - intros EQ. rewrite <- EQ. apply gcd_divide_r. + intros n m Hn. split. + - intros (q,Hq). rewrite Hq. + rewrite mul_comm. now apply gcd_mul_diag_l. + - intros EQ. rewrite <- EQ. apply gcd_divide_r. Qed. End NZGcdProp. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 794851a9dd..1951cfc3ef 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -40,10 +40,10 @@ Module Type NZLog2Prop Lemma log2_nonneg : forall a, 0 <= log2 a. Proof. intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite log2_nonpos. - destruct (log2_spec a Ha) as (_,LT). - apply lt_succ_r, (pow_gt_1 2). order'. - rewrite <- le_succ_l, <- one_succ in Ha. order. + - now rewrite log2_nonpos. + - destruct (log2_spec a Ha) as (_,LT). + apply lt_succ_r, (pow_gt_1 2). + order'. + + rewrite <- le_succ_l, <- one_succ in Ha. order. Qed. (** A tactic for proving positivity and non-negativity *) @@ -62,17 +62,17 @@ Lemma log2_unique : forall a b, 0<=b -> 2^b<=a<2^(S b) -> log2 a == b. Proof. intros a b Hb (LEb,LTb). assert (Ha : 0 < a). - apply lt_le_trans with (2^b); trivial. - apply pow_pos_nonneg; order'. - assert (Hc := log2_nonneg a). - destruct (log2_spec a Ha) as (LEc,LTc). - assert (log2 a <= b). - apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. - now apply le_le_succ_r. - assert (b <= log2 a). - apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. - now apply le_le_succ_r. - order. + - apply lt_le_trans with (2^b); trivial. + apply pow_pos_nonneg; order'. + - assert (Hc := log2_nonneg a). + destruct (log2_spec a Ha) as (LEc,LTc). + assert (log2 a <= b). + + apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. + now apply le_le_succ_r. + + assert (b <= log2 a). + * apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. + now apply le_le_succ_r. + * order. Qed. (** Hence log2 is a morphism. *) @@ -81,9 +81,9 @@ Instance log2_wd : Proper (eq==>eq) log2. Proof. intros x x' Hx. destruct (le_gt_cases x 0). - rewrite 2 log2_nonpos; trivial. reflexivity. now rewrite <- Hx. - apply log2_unique. apply log2_nonneg. - rewrite Hx in *. now apply log2_spec. + - rewrite 2 log2_nonpos; trivial. + reflexivity. + now rewrite <- Hx. + - apply log2_unique. + apply log2_nonneg. + + rewrite Hx in *. now apply log2_spec. Qed. (** An alternate specification *) @@ -95,24 +95,24 @@ Proof. destruct (log2_spec _ Ha) as (LE,LT). destruct (le_exists_sub _ _ LE) as (r & Hr & Hr'). exists r. - split. now rewrite add_comm. - split. trivial. - apply (add_lt_mono_r _ _ (2^log2 a)). - rewrite <- Hr. generalize LT. - rewrite pow_succ_r by order_pos. - rewrite two_succ at 1. now nzsimpl. + split. - now rewrite add_comm. + - split. + trivial. + + apply (add_lt_mono_r _ _ (2^log2 a)). + rewrite <- Hr. generalize LT. + rewrite pow_succ_r by order_pos. + rewrite two_succ at 1. now nzsimpl. Qed. Lemma log2_unique' : forall a b c, 0<=b -> 0<=c<2^b -> a == 2^b + c -> log2 a == b. Proof. intros a b c Hb (Hc,H) EQ. - apply log2_unique. trivial. - rewrite EQ. - split. - rewrite <- add_0_r at 1. now apply add_le_mono_l. - rewrite pow_succ_r by order. - rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l. + apply log2_unique. - trivial. + - rewrite EQ. + split. + + rewrite <- add_0_r at 1. now apply add_le_mono_l. + + rewrite pow_succ_r by order. + rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l. Qed. (** log2 is exact on powers of 2 *) @@ -121,7 +121,7 @@ Lemma log2_pow2 : forall a, 0<=a -> log2 (2^a) == a. Proof. intros a Ha. apply log2_unique' with 0; trivial. - split; order_pos. now nzsimpl. + - split; order_pos. - now nzsimpl. Qed. (** log2 and predecessors of powers of 2 *) @@ -131,12 +131,12 @@ Proof. intros a Ha. assert (Ha' : S (P a) == a) by (now rewrite lt_succ_pred with 0). apply log2_unique. - apply lt_succ_r; order. - rewrite <-le_succ_l, <-lt_succ_r, Ha'. - rewrite lt_succ_pred with 0. - split; try easy. apply pow_lt_mono_r_iff; try order'. - rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r. - apply pow_pos_nonneg; order'. + - apply lt_succ_r; order. + - rewrite <-le_succ_l, <-lt_succ_r, Ha'. + rewrite lt_succ_pred with 0. + + split; try easy. apply pow_lt_mono_r_iff; try order'. + rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r. + + apply pow_pos_nonneg; order'. Qed. (** log2 and basic constants *) @@ -167,11 +167,11 @@ Qed. Lemma log2_null : forall a, log2 a == 0 <-> a <= 1. Proof. intros a. split; intros H. - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. - generalize (log2_pos a Ha); order. - le_elim H. - apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ. - rewrite H. apply log2_1. + - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. + generalize (log2_pos a Ha); order. + - le_elim H. + + apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ. + + rewrite H. apply log2_1. Qed. (** log2 is a monotone function (but not a strict one) *) @@ -180,11 +180,11 @@ Lemma log2_le_mono : forall a b, a<=b -> log2 a <= log2 b. Proof. intros a b H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite log2_nonpos; order_pos. - assert (Hb : 0 < b) by order. - destruct (log2_spec a Ha) as (LEa,_). - destruct (log2_spec b Hb) as (_,LTb). - apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos. + - rewrite log2_nonpos; order_pos. + - assert (Hb : 0 < b) by order. + destruct (log2_spec a Ha) as (LEa,_). + destruct (log2_spec b Hb) as (_,LTb). + apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos. Qed. (** No reverse result for <=, consider for instance log2 3 <= log2 2 *) @@ -193,13 +193,13 @@ Lemma log2_lt_cancel : forall a b, log2 a < log2 b -> a < b. Proof. intros a b H. destruct (le_gt_cases b 0) as [Hb|Hb]. - rewrite (log2_nonpos b) in H; trivial. - generalize (log2_nonneg a); order. - destruct (le_gt_cases a 0) as [Ha|Ha]. order. - destruct (log2_spec a Ha) as (_,LTa). - destruct (log2_spec b Hb) as (LEb,_). - apply le_succ_l in H. - apply (pow_le_mono_r_iff 2) in H; order_pos. + - rewrite (log2_nonpos b) in H; trivial. + generalize (log2_nonneg a); order. + - destruct (le_gt_cases a 0) as [Ha|Ha]. + order. + + destruct (log2_spec a Ha) as (_,LTa). + destruct (log2_spec b Hb) as (LEb,_). + apply le_succ_l in H. + apply (pow_le_mono_r_iff 2) in H; order_pos. Qed. (** When left side is a power of 2, we have an equivalence for <= *) @@ -208,12 +208,12 @@ Lemma log2_le_pow2 : forall a b, 0<a -> (2^b<=a <-> b <= log2 a). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - generalize (log2_nonneg a); order. - rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono. - transitivity (2^(log2 a)). - apply pow_le_mono_r; order'. - now destruct (log2_spec a Ha). + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + generalize (log2_nonneg a); order. + + rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono. + - transitivity (2^(log2 a)). + + apply pow_le_mono_r; order'. + + now destruct (log2_spec a Ha). Qed. (** When right side is a square, we have an equivalence for < *) @@ -222,15 +222,15 @@ Lemma log2_lt_pow2 : forall a b, 0<a -> (a<2^b <-> log2 a < b). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite pow_neg_r in H; order. - apply (pow_lt_mono_r_iff 2); try order_pos. - apply le_lt_trans with a; trivial. - now destruct (log2_spec a Ha). - destruct (lt_ge_cases b 0) as [Hb|Hb]. - generalize (log2_nonneg a); order. - apply log2_lt_cancel; try order. - now rewrite log2_pow2. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + rewrite pow_neg_r in H; order. + + apply (pow_lt_mono_r_iff 2); try order_pos. + apply le_lt_trans with a; trivial. + now destruct (log2_spec a Ha). + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + generalize (log2_nonneg a); order. + + apply log2_lt_cancel; try order. + now rewrite log2_pow2. Qed. (** Comparing log2 and identity *) @@ -240,16 +240,16 @@ Proof. intros a Ha. apply (pow_lt_mono_r_iff 2); try order_pos. apply le_lt_trans with a. - now destruct (log2_spec a Ha). - apply pow_gt_lin_r; order'. + - now destruct (log2_spec a Ha). + - apply pow_gt_lin_r; order'. Qed. Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a. Proof. intros a Ha. le_elim Ha. - now apply lt_le_incl, log2_lt_lin. - rewrite <- Ha, log2_nonpos; order. + - now apply lt_le_incl, log2_lt_lin. + - rewrite <- Ha, log2_nonpos; order. Qed. (** Log2 and multiplication. *) @@ -271,14 +271,14 @@ Lemma log2_mul_above : forall a b, 0<=a -> 0<=b -> Proof. intros a b Ha Hb. le_elim Ha. - le_elim Hb. - apply lt_succ_r. - rewrite add_1_r, <- add_succ_r, <- add_succ_l. - apply log2_lt_pow2; try order_pos. - rewrite pow_add_r by order_pos. - apply mul_lt_mono_nonneg; try order; now apply log2_spec. - rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos. - rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos. + - le_elim Hb. + + apply lt_succ_r. + rewrite add_1_r, <- add_succ_r, <- add_succ_l. + apply log2_lt_pow2; try order_pos. + rewrite pow_add_r by order_pos. + apply mul_lt_mono_nonneg; try order; now apply log2_spec. + + rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos. + - rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos. Qed. (** And we can't find better approximations in general. @@ -293,10 +293,10 @@ Lemma log2_mul_pow2 : forall a b, 0<a -> 0<=b -> log2 (a*2^b) == b + log2 a. Proof. intros a b Ha Hb. apply log2_unique; try order_pos. split. - rewrite pow_add_r, mul_comm; try order_pos. - apply mul_le_mono_nonneg_r. order_pos. now apply log2_spec. - rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos. - apply mul_lt_mono_pos_l. order_pos. now apply log2_spec. + - rewrite pow_add_r, mul_comm; try order_pos. + apply mul_le_mono_nonneg_r. + order_pos. + now apply log2_spec. + - rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos. + apply mul_lt_mono_pos_l. + order_pos. + now apply log2_spec. Qed. Lemma log2_double : forall a, 0<a -> log2 (2*a) == S (log2 a). @@ -323,13 +323,13 @@ Lemma log2_succ_le : forall a, log2 (S a) <= S (log2 a). Proof. intros a. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. - apply (pow_le_mono_r_iff 2); try order_pos. - transitivity (S a). - apply log2_spec. - apply lt_succ_r; order. - now apply le_succ_l, log2_spec. - rewrite <- EQ, <- one_succ, log2_1; order_pos. - rewrite 2 log2_nonpos. order_pos. order'. now rewrite le_succ_l. + - apply (pow_le_mono_r_iff 2); try order_pos. + transitivity (S a). + + apply log2_spec. + apply lt_succ_r; order. + + now apply le_succ_l, log2_spec. + - rewrite <- EQ, <- one_succ, log2_1; order_pos. + - rewrite 2 log2_nonpos. + order_pos. + order'. + now rewrite le_succ_l. Qed. Lemma log2_succ_or : forall a, @@ -337,8 +337,8 @@ Lemma log2_succ_or : forall a, Proof. intros. destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H]. - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_succ_le a); order. + - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (log2_succ_le a); order. Qed. Lemma log2_eq_succ_is_pow2 : forall a, @@ -346,27 +346,27 @@ Lemma log2_eq_succ_is_pow2 : forall a, Proof. intros a H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite 2 (proj2 (log2_null _)) in H. generalize (lt_succ_diag_r 0); order. - order'. apply le_succ_l. order'. - assert (Ha' : 0 < S a) by (apply lt_succ_r; order). - exists (log2 (S a)). - generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)). - rewrite <- le_succ_l, <- H. order. + - rewrite 2 (proj2 (log2_null _)) in H. + generalize (lt_succ_diag_r 0); order. + + order'. + apply le_succ_l. order'. + - assert (Ha' : 0 < S a) by (apply lt_succ_r; order). + exists (log2 (S a)). + generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)). + rewrite <- le_succ_l, <- H. order. Qed. Lemma log2_eq_succ_iff_pow2 : forall a, 0<a -> (log2 (S a) == S (log2 a) <-> exists b, S a == 2^b). Proof. intros a Ha. - split. apply log2_eq_succ_is_pow2. - intros (b,Hb). - assert (Hb' : 0 < b). - apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono. - rewrite Hb, log2_pow2; try order'. - setoid_replace a with (P (2^b)). rewrite log2_pred_pow2; trivial. - symmetry; now apply lt_succ_pred with 0. - apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0. - rewrite <- Hb, lt_succ_r; order. + split. - apply log2_eq_succ_is_pow2. + - intros (b,Hb). + assert (Hb' : 0 < b). + + apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono. + + rewrite Hb, log2_pow2; try order'. + setoid_replace a with (P (2^b)). * rewrite log2_pred_pow2; trivial. + symmetry; now apply lt_succ_pred with 0. + * apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0. + rewrite <- Hb, lt_succ_r; order. Qed. Lemma log2_succ_double : forall a, 0<a -> log2 (2*a+1) == S (log2 a). @@ -376,18 +376,18 @@ Proof. destruct (log2_succ_or (2*a)) as [H|H]; [exfalso|now rewrite H, log2_double]. apply log2_eq_succ_is_pow2 in H. destruct H as (b,H). destruct (lt_trichotomy b 0) as [LT|[EQ|LT]]. - rewrite pow_neg_r in H; trivial. - apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. - rewrite <- one_succ in Ha. order'. - rewrite EQ, pow_0_r in H. - apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. - rewrite <- one_succ in Ha. order'. - assert (EQ:=lt_succ_pred 0 b LT). - rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ]. - destruct (lt_ge_cases a (2^(P b))) as [LT'|LE']. - generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order. - rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'. - rewrite <- H in LE'. apply le_succ_l in LE'. order. + - rewrite pow_neg_r in H; trivial. + apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. + rewrite <- one_succ in Ha. order'. + - rewrite EQ, pow_0_r in H. + apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'. + rewrite <- one_succ in Ha. order'. + - assert (EQ:=lt_succ_pred 0 b LT). + rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ]. + destruct (lt_ge_cases a (2^(P b))) as [LT'|LE']. + + generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order. + + rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'. + rewrite <- H in LE'. apply le_succ_l in LE'. order. Qed. (** Log2 and addition *) @@ -396,25 +396,28 @@ Lemma log2_add_le : forall a b, a~=1 -> b~=1 -> log2 (a+b) <= log2 a + log2 b. Proof. intros a b Ha Hb. destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|]. - rewrite one_succ, lt_succ_r in Ha'. - rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono. - rewrite <- (add_0_l b) at 2. now apply add_le_mono. - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. - rewrite one_succ, lt_succ_r in Hb'. - rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono. - rewrite <- (add_0_r a) at 2. now apply add_le_mono. - clear Ha Hb. - apply lt_succ_r. - apply log2_lt_pow2; try order_pos. - rewrite pow_succ_r by order_pos. - rewrite two_succ, one_succ at 1. nzsimpl. - apply add_lt_mono. - apply lt_le_trans with (2^(S (log2 a))). apply log2_spec; order'. - apply pow_le_mono_r. order'. rewrite <- add_1_r. apply add_le_mono_l. - rewrite one_succ; now apply le_succ_l, log2_pos. - apply lt_le_trans with (2^(S (log2 b))). apply log2_spec; order'. - apply pow_le_mono_r. order'. rewrite <- add_1_l. apply add_le_mono_r. - rewrite one_succ; now apply le_succ_l, log2_pos. + - rewrite one_succ, lt_succ_r in Ha'. + rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono. + rewrite <- (add_0_l b) at 2. now apply add_le_mono. + - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. + + rewrite one_succ, lt_succ_r in Hb'. + rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono. + rewrite <- (add_0_r a) at 2. now apply add_le_mono. + + clear Ha Hb. + apply lt_succ_r. + apply log2_lt_pow2; try order_pos. + rewrite pow_succ_r by order_pos. + rewrite two_succ, one_succ at 1. nzsimpl. + apply add_lt_mono. + * apply lt_le_trans with (2^(S (log2 a))). -- apply log2_spec; order'. + -- apply pow_le_mono_r. ++ order'. + ++ rewrite <- add_1_r. apply add_le_mono_l. + rewrite one_succ; now apply le_succ_l, log2_pos. + * apply lt_le_trans with (2^(S (log2 b))). + -- apply log2_spec; order'. + -- apply pow_le_mono_r. ++ order'. + ++ rewrite <- add_1_l. apply add_le_mono_r. + rewrite one_succ; now apply le_succ_l, log2_pos. Qed. (** The sum of two log2 is less than twice the log2 of the sum. @@ -430,17 +433,17 @@ Lemma add_log2_lt : forall a b, 0<a -> 0<b -> Proof. intros a b Ha Hb. nzsimpl'. assert (H : log2 a <= log2 (a+b)). - apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. - assert (H' : log2 b <= log2 (a+b)). - apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - le_elim H. - apply lt_le_trans with (log2 (a+b) + log2 b). - now apply add_lt_mono_r. now apply add_le_mono_l. - rewrite <- H at 1. apply add_lt_mono_l. - le_elim H'; trivial. - symmetry in H. apply log2_same in H; try order_pos. - symmetry in H'. apply log2_same in H'; try order_pos. - revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. + - apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. + - assert (H' : log2 b <= log2 (a+b)). + + apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + + le_elim H. + * apply lt_le_trans with (log2 (a+b) + log2 b). + -- now apply add_lt_mono_r. -- now apply add_le_mono_l. + * rewrite <- H at 1. apply add_lt_mono_l. + le_elim H'; trivial. + symmetry in H. apply log2_same in H; try order_pos. + symmetry in H'. apply log2_same in H'; try order_pos. + revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. Qed. End NZLog2Prop. @@ -493,9 +496,9 @@ Qed. Instance log2_up_wd : Proper (eq==>eq) log2_up. Proof. assert (Proper (eq==>eq==>Logic.eq) compare). - repeat red; intros; do 2 case compare_spec; trivial; order. - intros a a' Ha. unfold log2_up. rewrite Ha at 1. - case compare; now rewrite ?Ha. + - repeat red; intros; do 2 case compare_spec; trivial; order. + - intros a a' Ha. unfold log2_up. rewrite Ha at 1. + case compare; now rewrite ?Ha. Qed. (** [log2_up] is always non-negative *) @@ -512,22 +515,23 @@ Lemma log2_up_unique : forall a b, 0<b -> 2^(P b)<a<=2^b -> log2_up a == b. Proof. intros a b Hb (LEb,LTb). assert (Ha : 1 < a). - apply le_lt_trans with (2^(P b)); trivial. - rewrite one_succ. apply le_succ_l. - apply pow_pos_nonneg. order'. apply lt_succ_r. - now rewrite (lt_succ_pred 0 b Hb). - assert (Hc := log2_up_nonneg a). - destruct (log2_up_spec a Ha) as (LTc,LEc). - assert (b <= log2_up a). - apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb). - rewrite <- succ_lt_mono. - apply (pow_lt_mono_r_iff 2); try order'. - assert (Hc' : 0 < log2_up a) by order. - assert (log2_up a <= b). - apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc'). - rewrite <- succ_lt_mono. - apply (pow_lt_mono_r_iff 2); try order'. - order. + - apply le_lt_trans with (2^(P b)); trivial. + rewrite one_succ. apply le_succ_l. + apply pow_pos_nonneg. + order'. + + apply lt_succ_r. + now rewrite (lt_succ_pred 0 b Hb). + - assert (Hc := log2_up_nonneg a). + destruct (log2_up_spec a Ha) as (LTc,LEc). + assert (b <= log2_up a). + + apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb). + rewrite <- succ_lt_mono. + apply (pow_lt_mono_r_iff 2); try order'. + + assert (Hc' : 0 < log2_up a) by order. + assert (log2_up a <= b). + * apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc'). + rewrite <- succ_lt_mono. + apply (pow_lt_mono_r_iff 2); try order'. + * order. Qed. (** [log2_up] is exact on powers of 2 *) @@ -536,12 +540,12 @@ Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a. Proof. intros a Ha. le_elim Ha. - apply log2_up_unique; trivial. - split; try order. - apply pow_lt_mono_r; try order'. - rewrite <- (lt_succ_pred 0 a Ha) at 2. - now apply lt_succ_r. - now rewrite <- Ha, pow_0_r, log2_up_eqn0. + - apply log2_up_unique; trivial. + split; try order. + apply pow_lt_mono_r; try order'. + rewrite <- (lt_succ_pred 0 a Ha) at 2. + now apply lt_succ_r. + - now rewrite <- Ha, pow_0_r, log2_up_eqn0. Qed. (** [log2_up] and successors of powers of 2 *) @@ -570,9 +574,9 @@ Qed. Lemma le_log2_log2_up : forall a, log2 a <= log2_up a. Proof. intros a. unfold log2_up. case compare_spec; intros H. - rewrite <- H, log2_1. order. - rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le. - rewrite log2_nonpos. order. now rewrite <-lt_succ_r, <-one_succ. + - rewrite <- H, log2_1. order. + - rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le. + - rewrite log2_nonpos. + order. + now rewrite <-lt_succ_r, <-one_succ. Qed. Lemma le_log2_up_succ_log2 : forall a, log2_up a <= S (log2 a). @@ -586,23 +590,24 @@ Lemma log2_log2_up_spec : forall a, 0<a -> 2^log2 a <= a <= 2^log2_up a. Proof. intros a H. split. - now apply log2_spec. - rewrite <-le_succ_l, <-one_succ in H. le_elim H. - now apply log2_up_spec. - now rewrite <-H, log2_up_1, pow_0_r. + - now apply log2_spec. + - rewrite <-le_succ_l, <-one_succ in H. le_elim H. + + now apply log2_up_spec. + + now rewrite <-H, log2_up_1, pow_0_r. Qed. Lemma log2_log2_up_exact : forall a, 0<a -> (log2 a == log2_up a <-> exists b, a == 2^b). Proof. intros a Ha. - split. intros. exists (log2 a). - generalize (log2_log2_up_spec a Ha). rewrite <-H. - destruct 1; order. - intros (b,Hb). rewrite Hb. - destruct (le_gt_cases 0 b). - now rewrite log2_pow2, log2_up_pow2. - rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos. + split. + - intros. exists (log2 a). + generalize (log2_log2_up_spec a Ha). rewrite <-H. + destruct 1; order. + - intros (b,Hb). rewrite Hb. + destruct (le_gt_cases 0 b). + + now rewrite log2_pow2, log2_up_pow2. + + rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos. Qed. (** [log2_up] n is strictly positive for 1<n *) @@ -617,9 +622,9 @@ Qed. Lemma log2_up_null : forall a, log2_up a == 0 <-> a <= 1. Proof. intros a. split; intros H. - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. - generalize (log2_up_pos a Ha); order. - now apply log2_up_eqn0. + - destruct (le_gt_cases a 1) as [Ha|Ha]; trivial. + generalize (log2_up_pos a Ha); order. + - now apply log2_up_eqn0. Qed. (** [log2_up] is a monotone function (but not a strict one) *) @@ -628,10 +633,10 @@ Lemma log2_up_le_mono : forall a b, a<=b -> log2_up a <= log2_up b. Proof. intros a b H. destruct (le_gt_cases a 1) as [Ha|Ha]. - rewrite log2_up_eqn0; trivial. apply log2_up_nonneg. - rewrite 2 log2_up_eqn; try order. - rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono. - rewrite 2 lt_succ_pred with 1; order. + - rewrite log2_up_eqn0; trivial. apply log2_up_nonneg. + - rewrite 2 log2_up_eqn; try order. + rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono. + rewrite 2 lt_succ_pred with 1; order. Qed. (** No reverse result for <=, consider for instance log2_up 4 <= log2_up 3 *) @@ -640,12 +645,12 @@ Lemma log2_up_lt_cancel : forall a b, log2_up a < log2_up b -> a < b. Proof. intros a b H. destruct (le_gt_cases b 1) as [Hb|Hb]. - rewrite (log2_up_eqn0 b) in H; trivial. - generalize (log2_up_nonneg a); order. - destruct (le_gt_cases a 1) as [Ha|Ha]. order. - rewrite 2 log2_up_eqn in H; try order. - rewrite <- succ_lt_mono in H. apply log2_lt_cancel, succ_lt_mono in H. - rewrite 2 lt_succ_pred with 1 in H; order. + - rewrite (log2_up_eqn0 b) in H; trivial. + generalize (log2_up_nonneg a); order. + - destruct (le_gt_cases a 1) as [Ha|Ha]. + order. + + rewrite 2 log2_up_eqn in H; try order. + rewrite <- succ_lt_mono in H. apply log2_lt_cancel, succ_lt_mono in H. + rewrite 2 lt_succ_pred with 1 in H; order. Qed. (** When left side is a power of 2, we have an equivalence for < *) @@ -654,16 +659,16 @@ Lemma log2_up_lt_pow2 : forall a b, 0<a -> (2^b<a <-> b < log2_up a). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - generalize (log2_up_nonneg a); order. - apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg. - apply lt_le_trans with a; trivial. - apply (log2_up_spec a). - apply le_lt_trans with (2^b); trivial. - rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - now rewrite pow_neg_r. - rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + generalize (log2_up_nonneg a); order. + + apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg. + * apply lt_le_trans with a; trivial. + apply (log2_up_spec a). + apply le_lt_trans with (2^b); trivial. + rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + now rewrite pow_neg_r. + + rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel. Qed. (** When right side is a square, we have an equivalence for <= *) @@ -672,12 +677,12 @@ Lemma log2_up_le_pow2 : forall a b, 0<a -> (a<=2^b <-> log2_up a <= b). Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite pow_neg_r in H; order. - rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono. - transitivity (2^(log2_up a)). - now apply log2_log2_up_spec. - apply pow_le_mono_r; order'. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + rewrite pow_neg_r in H; order. + + rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono. + - transitivity (2^(log2_up a)). + + now apply log2_log2_up_spec. + + apply pow_le_mono_r; order'. Qed. (** Comparing [log2_up] and identity *) @@ -688,15 +693,15 @@ Proof. assert (H : S (P a) == a) by (now apply lt_succ_pred with 0). rewrite <- H at 2. apply lt_succ_r. apply log2_up_le_pow2; trivial. rewrite <- H at 1. apply le_succ_l. - apply pow_gt_lin_r. order'. apply lt_succ_r; order. + apply pow_gt_lin_r. - order'. - apply lt_succ_r; order. Qed. Lemma log2_up_le_lin : forall a, 0<=a -> log2_up a <= a. Proof. intros a Ha. le_elim Ha. - now apply lt_le_incl, log2_up_lt_lin. - rewrite <- Ha, log2_up_nonpos; order. + - now apply lt_le_incl, log2_up_lt_lin. + - rewrite <- Ha, log2_up_nonpos; order. Qed. (** [log2_up] and multiplication. *) @@ -711,12 +716,12 @@ Proof. assert (Ha':=log2_up_nonneg a). assert (Hb':=log2_up_nonneg b). le_elim Ha. - le_elim Hb. - apply log2_up_le_pow2; try order_pos. - rewrite pow_add_r; trivial. - apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'. - rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos. - rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos. + - le_elim Hb. + + apply log2_up_le_pow2; try order_pos. + rewrite pow_add_r; trivial. + apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'. + + rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos. + - rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos. Qed. Lemma log2_up_mul_below : forall a b, 0<a -> 0<b -> @@ -724,21 +729,21 @@ Lemma log2_up_mul_below : forall a b, 0<a -> 0<b -> Proof. intros a b Ha Hb. rewrite <-le_succ_l, <-one_succ in Ha. le_elim Ha. - rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb. - assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial). - assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial). - rewrite <- (lt_succ_pred 0 (log2_up a)); trivial. - rewrite <- (lt_succ_pred 0 (log2_up b)); trivial. - nzsimpl. rewrite <- succ_le_mono, le_succ_l. - apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg. - rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial). - apply lt_le_trans with (a*b). - apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec. - apply log2_up_spec. - setoid_replace 1 with (1*1) by now nzsimpl. - apply mul_lt_mono_nonneg; order'. - rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r. - rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r. + - rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb. + + assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial). + assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial). + rewrite <- (lt_succ_pred 0 (log2_up a)); trivial. + rewrite <- (lt_succ_pred 0 (log2_up b)); trivial. + nzsimpl. rewrite <- succ_le_mono, le_succ_l. + apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg. + * rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial). + apply lt_le_trans with (a*b). + -- apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec. + -- apply log2_up_spec. + setoid_replace 1 with (1*1) by now nzsimpl. + apply mul_lt_mono_nonneg; order'. + + rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r. + - rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r. Qed. (** And we can't find better approximations in general. @@ -754,16 +759,16 @@ Lemma log2_up_mul_pow2 : forall a b, 0<a -> 0<=b -> Proof. intros a b Ha Hb. rewrite <- le_succ_l, <- one_succ in Ha; le_elim Ha. - apply log2_up_unique. apply add_nonneg_pos; trivial. now apply log2_up_pos. - split. - assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)). - rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial. - apply mul_lt_mono_pos_r. order_pos. now apply log2_up_spec. - rewrite <- lt_succ_r, EQ. now apply log2_up_pos. - rewrite pow_add_r, mul_comm; trivial. - apply mul_le_mono_nonneg_l. order_pos. now apply log2_up_spec. - apply log2_up_nonneg. - now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2. + - apply log2_up_unique. + apply add_nonneg_pos; trivial. now apply log2_up_pos. + + split. + * assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)). + rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial. + -- apply mul_lt_mono_pos_r. ++ order_pos. ++ now apply log2_up_spec. + -- rewrite <- lt_succ_r, EQ. now apply log2_up_pos. + * rewrite pow_add_r, mul_comm; trivial. + -- apply mul_le_mono_nonneg_l. ++ order_pos. ++ now apply log2_up_spec. + -- apply log2_up_nonneg. + - now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2. Qed. Lemma log2_up_double : forall a, 0<a -> log2_up (2*a) == S (log2_up a). @@ -790,12 +795,12 @@ Lemma log2_up_succ_le : forall a, log2_up (S a) <= S (log2_up a). Proof. intros a. destruct (lt_trichotomy 1 a) as [LT|[EQ|LT]]. - rewrite 2 log2_up_eqn; trivial. - rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1. - apply log2_succ_le. - apply lt_succ_r; order. - rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'. - rewrite 2 log2_up_eqn0. order_pos. order'. now rewrite le_succ_l. + - rewrite 2 log2_up_eqn; trivial. + + rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1. + apply log2_succ_le. + + apply lt_succ_r; order. + - rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'. + - rewrite 2 log2_up_eqn0. + order_pos. + order'. + now rewrite le_succ_l. Qed. Lemma log2_up_succ_or : forall a, @@ -803,8 +808,8 @@ Lemma log2_up_succ_or : forall a, Proof. intros. destruct (le_gt_cases (log2_up (S a)) (log2_up a)). - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. + - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. Qed. Lemma log2_up_eq_succ_is_pow2 : forall a, @@ -812,33 +817,33 @@ Lemma log2_up_eq_succ_is_pow2 : forall a, Proof. intros a H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite 2 (proj2 (log2_up_null _)) in H. generalize (lt_succ_diag_r 0); order. - order'. apply le_succ_l. order'. - assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono). - exists (log2_up a). - generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)). - rewrite H, pred_succ, lt_succ_r. order. + - rewrite 2 (proj2 (log2_up_null _)) in H. + generalize (lt_succ_diag_r 0); order. + + order'. + apply le_succ_l. order'. + - assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono). + exists (log2_up a). + generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)). + rewrite H, pred_succ, lt_succ_r. order. Qed. Lemma log2_up_eq_succ_iff_pow2 : forall a, 0<a -> (log2_up (S a) == S (log2_up a) <-> exists b, a == 2^b). Proof. intros a Ha. - split. apply log2_up_eq_succ_is_pow2. - intros (b,Hb). - destruct (lt_ge_cases b 0) as [Hb'|Hb']. - rewrite pow_neg_r in Hb; order. - rewrite Hb, log2_up_pow2; try order'. - now rewrite log2_up_succ_pow2. + split. - apply log2_up_eq_succ_is_pow2. + - intros (b,Hb). + destruct (lt_ge_cases b 0) as [Hb'|Hb']. + + rewrite pow_neg_r in Hb; order. + + rewrite Hb, log2_up_pow2; try order'. + now rewrite log2_up_succ_pow2. Qed. Lemma log2_up_succ_double : forall a, 0<a -> log2_up (2*a+1) == 2 + log2 a. Proof. intros a Ha. - rewrite log2_up_eqn. rewrite add_1_r, pred_succ, log2_double; now nzsimpl'. - apply le_lt_trans with (0+1). now nzsimpl'. - apply add_lt_mono_r. order_pos. + rewrite log2_up_eqn. - rewrite add_1_r, pred_succ, log2_double; now nzsimpl'. + - apply le_lt_trans with (0+1). + now nzsimpl'. + + apply add_lt_mono_r. order_pos. Qed. (** [log2_up] and addition *) @@ -848,17 +853,17 @@ Lemma log2_up_add_le : forall a b, a~=1 -> b~=1 -> Proof. intros a b Ha Hb. destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|]. - rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono. - rewrite one_succ, lt_succ_r in Ha'. - rewrite <- (add_0_l b) at 2. now apply add_le_mono. - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. - rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono. - rewrite one_succ, lt_succ_r in Hb'. - rewrite <- (add_0_r a) at 2. now apply add_le_mono. - clear Ha Hb. - transitivity (log2_up (a*b)). - now apply log2_up_le_mono, add_le_mul. - apply log2_up_mul_above; order'. + - rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono. + rewrite one_succ, lt_succ_r in Ha'. + rewrite <- (add_0_l b) at 2. now apply add_le_mono. + - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. + + rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono. + rewrite one_succ, lt_succ_r in Hb'. + rewrite <- (add_0_r a) at 2. now apply add_le_mono. + + clear Ha Hb. + transitivity (log2_up (a*b)). + * now apply log2_up_le_mono, add_le_mul. + * apply log2_up_mul_above; order'. Qed. (** The sum of two [log2_up] is less than twice the [log2_up] of the sum. @@ -874,17 +879,17 @@ Lemma add_log2_up_lt : forall a b, 0<a -> 0<b -> Proof. intros a b Ha Hb. nzsimpl'. assert (H : log2_up a <= log2_up (a+b)). - apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. - assert (H' : log2_up b <= log2_up (a+b)). - apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - le_elim H. - apply lt_le_trans with (log2_up (a+b) + log2_up b). - now apply add_lt_mono_r. now apply add_le_mono_l. - rewrite <- H at 1. apply add_lt_mono_l. - le_elim H'. trivial. - symmetry in H. apply log2_up_same in H; try order_pos. - symmetry in H'. apply log2_up_same in H'; try order_pos. - revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. + - apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. + - assert (H' : log2_up b <= log2_up (a+b)). + + apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + + le_elim H. + * apply lt_le_trans with (log2_up (a+b) + log2_up b). + -- now apply add_lt_mono_r. -- now apply add_le_mono_l. + * rewrite <- H at 1. apply add_lt_mono_l. + le_elim H'. -- trivial. + -- symmetry in H. apply log2_up_same in H; try order_pos. + symmetry in H'. apply log2_up_same in H'; try order_pos. + revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. Qed. End NZLog2UpProp. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 44cbc51712..1492188452 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -22,24 +22,27 @@ Qed. Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. Proof. -intros n m; nzinduct n. now nzsimpl. -intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc. -now rewrite add_cancel_r. + intros n m; nzinduct n. + - now nzsimpl. + - intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc. + now rewrite add_cancel_r. Qed. Hint Rewrite mul_0_r mul_succ_r : nz. Theorem mul_comm : forall n m, n * m == m * n. Proof. -intros n m; nzinduct n. now nzsimpl. -intro. nzsimpl. now rewrite add_cancel_r. + intros n m; nzinduct n. + - now nzsimpl. + - intro. nzsimpl. now rewrite add_cancel_r. Qed. Theorem mul_add_distr_r : forall n m p, (n + m) * p == n * p + m * p. Proof. -intros n m p; nzinduct n. now nzsimpl. -intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc. -now rewrite add_cancel_r. + intros n m p; nzinduct n. + - now nzsimpl. + - intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc. + now rewrite add_cancel_r. Qed. Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p. @@ -51,9 +54,9 @@ Qed. Theorem mul_assoc : forall n m p, n * (m * p) == (n * m) * p. Proof. -intros n m p; nzinduct n. now nzsimpl. -intro n. nzsimpl. rewrite mul_add_distr_r. -now rewrite add_cancel_r. + intros n m p; nzinduct n. - now nzsimpl. + - intro n. nzsimpl. rewrite mul_add_distr_r. + now rewrite add_cancel_r. Qed. Theorem mul_1_l : forall n, 1 * n == n. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 292f0837c0..dc4167e96f 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -26,16 +26,16 @@ Qed. Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m). Proof. -intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). solve_proper. -intros. now nzsimpl. -clear p Hp. intros p Hp IH n m. nzsimpl. -assert (LR : forall n m, n < m -> p * n + n < p * m + m) - by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH). -split; intros H. -now apply LR. -destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. -rewrite EQ in H. order. -apply LR in GT. order. + intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). - solve_proper. + - intros. now nzsimpl. + - clear p Hp. intros p Hp IH n m. nzsimpl. + assert (LR : forall n m, n < m -> p * n + n < p * m + m) + by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH). + split; intros H. + + now apply LR. + + destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. + * rewrite EQ in H. order. + * apply LR in GT. order. Qed. Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p). @@ -47,19 +47,20 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. nzord_induct p. -order. -intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. -intros p Hp IH n m _. apply le_succ_l in Hp. -le_elim Hp. -assert (LR : forall n m, n < m -> p * m < p * n). - intros n1 m1 H. apply (le_lt_add_lt n1 m1). - now apply lt_le_incl. rewrite <- 2 mul_succ_l. now rewrite <- IH. -split; intros H. -now apply LR. -destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. -rewrite EQ in H. order. -apply LR in GT. order. -rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl. +- order. +- intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. +- intros p Hp IH n m _. apply le_succ_l in Hp. + le_elim Hp. + + assert (LR : forall n m, n < m -> p * m < p * n). + * intros n1 m1 H. apply (le_lt_add_lt n1 m1). + -- now apply lt_le_incl. + -- rewrite <- 2 mul_succ_l. now rewrite <- IH. + * split; intros H. + -- now apply LR. + -- destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. + ++ rewrite EQ in H. order. + ++ apply LR in GT. order. + + rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl. Qed. Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p). @@ -71,17 +72,17 @@ Qed. Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply mul_lt_mono_pos_l. -apply eq_le_incl; now rewrite H2. -apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l. +- le_elim H2. + apply lt_le_incl. now apply mul_lt_mono_pos_l. + + apply eq_le_incl; now rewrite H2. +- apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l. Qed. Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply mul_lt_mono_neg_l. -apply eq_le_incl; now rewrite H2. -apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l. +- le_elim H2. + apply lt_le_incl. now apply mul_lt_mono_neg_l. + + apply eq_le_incl; now rewrite H2. +- apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l. Qed. Theorem mul_le_mono_nonneg_r : forall n m p, 0 <= p -> n <= m -> n * p <= m * p. @@ -101,10 +102,10 @@ Proof. intros n m p Hp; split; intro H; [|now f_equiv]. apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp]; destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. -apply (mul_lt_mono_neg_l p) in LT; order. -apply (mul_lt_mono_neg_l p) in GT; order. -apply (mul_lt_mono_pos_l p) in LT; order. -apply (mul_lt_mono_pos_l p) in GT; order. +- apply (mul_lt_mono_neg_l p) in LT; order. +- apply (mul_lt_mono_neg_l p) in GT; order. +- apply (mul_lt_mono_pos_l p) in LT; order. +- apply (mul_lt_mono_pos_l p) in GT; order. Qed. Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m). @@ -155,8 +156,8 @@ Theorem mul_lt_mono_nonneg : Proof. intros n m p q H1 H2 H3 H4. apply le_lt_trans with (m * p). -apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. -apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n]. +- apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. +- apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n]. Qed. (* There are still many variants of the theorem above. One can assume 0 < n @@ -167,10 +168,10 @@ Theorem mul_le_mono_nonneg : Proof. intros n m p q H1 H2 H3 H4. le_elim H2; le_elim H4. -apply lt_le_incl; now apply mul_lt_mono_nonneg. -rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. -rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl]. -rewrite H2; rewrite H4; now apply eq_le_incl. +- apply lt_le_incl; now apply mul_lt_mono_nonneg. +- rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. +- rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl]. +- rewrite H2; rewrite H4; now apply eq_le_incl. Qed. Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m. @@ -225,29 +226,29 @@ Qed. Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m. Proof. intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1. -rewrite mul_1_l in H1. now apply lt_1_l with m. -assumption. +- rewrite mul_1_l in H1. now apply lt_1_l with m. +- assumption. Qed. Theorem eq_mul_0 : forall n m, n * m == 0 <-> n == 0 \/ m == 0. Proof. intros n m; split. -intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; -destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; -try (now right); try (now left). -exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |]. -exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |]. -exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |]. -exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |]. -intros [H | H]. now rewrite H, mul_0_l. now rewrite H, mul_0_r. +- intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; + destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; + try (now right); try (now left). + + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |]. + + exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |]. + + exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |]. + + exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |]. +- intros [H | H]. + now rewrite H, mul_0_l. + now rewrite H, mul_0_r. Qed. Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof. intros n m; split; intro H. -intro H1; apply eq_mul_0 in H1. tauto. -split; intro H1; rewrite H1 in H; -(rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H. +- intro H1; apply eq_mul_0 in H1. tauto. +- split; intro H1; rewrite H1 in H; + (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H. Qed. Theorem eq_square_0 : forall n, n * n == 0 <-> n == 0. @@ -258,13 +259,13 @@ Qed. Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0. Proof. intros n m H1 H2. apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. -assumption. false_hyp H1 H2. +- assumption. - false_hyp H1 H2. Qed. Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0. Proof. intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. -false_hyp H1 H2. assumption. +- false_hyp H1 H2. - assumption. Qed. (** Some alternative names: *) @@ -276,16 +277,16 @@ Definition mul_eq_0_r := eq_mul_0_r. Theorem lt_0_mul n m : 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). Proof. split; [intro H | intros [[H1 H2] | [H1 H2]]]. -destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; -[| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |]; -(destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; -[| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]); -try (left; now split); try (right; now split). -assert (H3 : n * m < 0) by now apply mul_neg_pos. -exfalso; now apply (lt_asymm (n * m) 0). -assert (H3 : n * m < 0) by now apply mul_pos_neg. -exfalso; now apply (lt_asymm (n * m) 0). -now apply mul_pos_pos. now apply mul_neg_neg. +- destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]]; + [| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |]; + (destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]]; + [| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]); + try (left; now split); try (right; now split). + + assert (H3 : n * m < 0) by now apply mul_neg_pos. + exfalso; now apply (lt_asymm (n * m) 0). + + assert (H3 : n * m < 0) by now apply mul_pos_neg. + exfalso; now apply (lt_asymm (n * m) 0). +- now apply mul_pos_pos. - now apply mul_neg_neg. Qed. Theorem square_lt_mono_nonneg : forall n m, 0 <= n -> n < m -> n * n < m * m. @@ -304,38 +305,38 @@ other variable *) Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). -now apply lt_le_trans with 0. -destruct (lt_ge_cases n m) as [LT|LE]; trivial. -apply square_le_mono_nonneg in LE; order. +- now apply lt_le_trans with 0. +- destruct (lt_ge_cases n m) as [LT|LE]; trivial. + apply square_le_mono_nonneg in LE; order. Qed. Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). -apply lt_le_incl; now apply lt_le_trans with 0. -destruct (le_gt_cases n m) as [LE|LT]; trivial. -apply square_lt_mono_nonneg in LT; order. +- apply lt_le_incl; now apply lt_le_trans with 0. +- destruct (le_gt_cases n m) as [LE|LT]; trivial. + apply square_lt_mono_nonneg in LT; order. Qed. Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m. Proof. intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two). -rewrite two_succ. nzsimpl. now rewrite le_succ_l. -order'. +- rewrite two_succ. nzsimpl. now rewrite le_succ_l. +- order'. Qed. Lemma add_le_mul : forall a b, 1<a -> 1<b -> a+b <= a*b. Proof. assert (AUX : forall a b, 0<a -> 0<b -> (S a)+(S b) <= (S a)*(S b)). - intros a b Ha Hb. - nzsimpl. rewrite <- succ_le_mono. apply le_succ_l. - rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b). - apply add_lt_mono_r. - now apply mul_pos_pos. - intros a b Ha Hb. - assert (Ha' := lt_succ_pred 1 a Ha). - assert (Hb' := lt_succ_pred 1 b Hb). - rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order. + - intros a b Ha Hb. + nzsimpl. rewrite <- succ_le_mono. apply le_succ_l. + rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b). + apply add_lt_mono_r. + now apply mul_pos_pos. + - intros a b Ha Hb. + assert (Ha' := lt_succ_pred 1 a Ha). + assert (Hb' := lt_succ_pred 1 b Hb). + rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order. Qed. (** A few results about squares *) @@ -343,25 +344,25 @@ Qed. Lemma square_nonneg : forall a, 0 <= a * a. Proof. intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). - now apply mul_le_mono_nonpos_l. - apply mul_le_mono_nonneg_l; order. + - now apply mul_le_mono_nonpos_l. + - apply mul_le_mono_nonneg_l; order. Qed. Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b. Proof. assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b). - intros a b (Ha,H). - destruct (le_exists_sub _ _ H) as (d & EQ & Hd). - rewrite EQ. - rewrite 2 mul_add_distr_r. - rewrite !add_assoc. apply add_le_mono_r. - rewrite add_comm. apply add_le_mono_l. - apply mul_le_mono_nonneg_l; trivial. order. - intros a b Ha Hb. - destruct (le_gt_cases a b). - apply AUX; split; order. - rewrite (add_comm (b*a)), (add_comm (a*a)). - apply AUX; split; order. + - intros a b (Ha,H). + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. order. + - intros a b Ha Hb. + destruct (le_gt_cases a b). + + apply AUX; split; order. + + rewrite (add_comm (b*a)), (add_comm (a*a)). + apply AUX; split; order. Qed. Lemma add_square_le : forall a b, 0<=a -> 0<=b -> diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 60e1123b35..89bc5cfecb 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -60,19 +60,19 @@ Qed. Theorem nle_succ_diag_l : forall n, ~ S n <= n. Proof. intros n H; le_elim H. -false_hyp H nlt_succ_diag_l. false_hyp H neq_succ_diag_l. ++ false_hyp H nlt_succ_diag_l. + false_hyp H neq_succ_diag_l. Qed. Theorem le_succ_l : forall n m, S n <= m <-> n < m. Proof. intro n; nzinduct m n. -split; intro H. false_hyp H nle_succ_diag_l. false_hyp H lt_irrefl. -intro m. -rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. -rewrite or_cancel_r. -reflexivity. -intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l. -intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl. +- split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl. +- intro m. + rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. + rewrite or_cancel_r. + + reflexivity. + + intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l. + + intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl. Qed. (** Trichotomy *) @@ -80,8 +80,8 @@ Qed. Theorem le_gt_cases : forall n m, n <= m \/ n > m. Proof. intros n m; nzinduct n m. -left; apply le_refl. -intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition. +- left; apply le_refl. +- intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition. Qed. Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n. @@ -96,14 +96,14 @@ Notation lt_eq_gt_cases := lt_trichotomy (only parsing). Theorem lt_asymm : forall n m, n < m -> ~ m < n. Proof. intros n m; nzinduct n m. -intros H; false_hyp H lt_irrefl. -intro n; split; intros H H1 H2. -apply lt_succ_r in H2. le_elim H2. -apply H; auto. apply le_succ_l. now apply lt_le_incl. -rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l. -apply le_succ_l in H1. le_elim H1. -apply H; auto. rewrite lt_succ_r. now apply lt_le_incl. -rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l. +- intros H; false_hyp H lt_irrefl. +- intro n; split; intros H H1 H2. + + apply lt_succ_r in H2. le_elim H2. + * apply H; auto. apply le_succ_l. now apply lt_le_incl. + * rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l. + + apply le_succ_l in H1. le_elim H1. + * apply H; auto. rewrite lt_succ_r. now apply lt_le_incl. + * rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l. Qed. Notation lt_ngt := lt_asymm (only parsing). @@ -111,13 +111,15 @@ Notation lt_ngt := lt_asymm (only parsing). Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. Proof. intros n m p; nzinduct p m. -intros _ H; false_hyp H lt_irrefl. -intro p. rewrite 2 lt_succ_r. -split; intros H H1 H2. -apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1]. -assert (n <= p) as H3 by (auto using lt_le_incl). -le_elim H3. assumption. rewrite <- H3 in H2. -elim (lt_asymm n m); auto. +- intros _ H; false_hyp H lt_irrefl. +- intro p. rewrite 2 lt_succ_r. + split; intros H H1 H2. + + apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1]. + + assert (n <= p) as H3 by (auto using lt_le_incl). + le_elim H3. + * assumption. + * rewrite <- H3 in H2. + elim (lt_asymm n m); auto. Qed. Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. @@ -130,16 +132,16 @@ Qed. (** Some type classes about order *) Instance lt_strorder : StrictOrder lt. -Proof. split. exact lt_irrefl. exact lt_trans. Qed. +Proof. split. - exact lt_irrefl. - exact lt_trans. Qed. Instance le_preorder : PreOrder le. -Proof. split. exact le_refl. exact le_trans. Qed. +Proof. split. - exact le_refl. - exact le_trans. Qed. Instance le_partialorder : PartialOrder _ le. Proof. intros x y. compute. split. -intro EQ; now rewrite EQ. -rewrite 2 lt_eq_cases. intuition. elim (lt_irrefl x). now transitivity y. +- intro EQ; now rewrite EQ. +- rewrite 2 lt_eq_cases. intuition. elim (lt_irrefl x). now transitivity y. Qed. (** We know enough now to benefit from the generic [order] tactic. *) @@ -246,7 +248,7 @@ Qed. Theorem lt_0_2 : 0 < 2. Proof. -transitivity 1. apply lt_0_1. apply lt_1_2. + transitivity 1. - apply lt_0_1. - apply lt_1_2. Qed. Theorem le_0_2 : 0 <= 2. @@ -300,9 +302,9 @@ Qed. Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m. Proof. intros n m; split; intro H. -destruct (eq_decidable n m) as [H1 | H1]. -assumption. false_hyp H1 H. -intro H1; now apply H1. +- destruct (eq_decidable n m) as [H1 | H1]. + + assumption. + false_hyp H1 H. +- intro H1; now apply H1. Qed. Theorem le_ngt : forall n m, n <= m <-> ~ n > m. @@ -321,8 +323,8 @@ Qed. Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m. Proof. intros n m; split; intro H. -destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. -intro H1; false_hyp H H1. +- destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. +- intro H1; false_hyp H H1. Qed. Theorem nle_gt : forall n m, ~ n <= m <-> n > m. @@ -341,8 +343,8 @@ Qed. Theorem le_dne : forall n m, ~ ~ n <= m <-> n <= m. Proof. intros n m; split; intro H. -destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. -intro H1; false_hyp H H1. +- destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H]. +- intro H1; false_hyp H H1. Qed. Theorem nlt_succ_r : forall n m, ~ m < S n <-> n < m. @@ -361,18 +363,18 @@ Lemma lt_exists_pred_strong : forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k. Proof. intro z; nzinduct n z. -order. -intro n; split; intros IH m H1 H2. -apply le_succ_r in H2. destruct H2 as [H2 | H2]. -now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2]. -apply IH. assumption. now apply le_le_succ_r. +- order. +- intro n; split; intros IH m H1 H2. + + apply le_succ_r in H2. destruct H2 as [H2 | H2]. + * now apply IH. * exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2]. + + apply IH. * assumption. * now apply le_le_succ_r. Qed. Theorem lt_exists_pred : forall z n, z < n -> exists k, n == S k /\ z <= k. Proof. intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). -assumption. apply le_refl. +- assumption. - apply le_refl. Qed. Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n. @@ -404,18 +406,19 @@ Let right_step'' := forall n, A' n <-> A' (S n). Lemma rs_rs' : A z -> right_step -> right_step'. Proof. intros Az RS n H1 H2. -le_elim H1. apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]]. -rewrite H3. apply RS; trivial. apply H2; trivial. -rewrite H3; apply lt_succ_diag_r. -rewrite <- H1; apply Az. +le_elim H1. +- apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]]. + rewrite H3. apply RS; trivial. apply H2; trivial. + rewrite H3; apply lt_succ_diag_r. +- rewrite <- H1; apply Az. Qed. Lemma rs'_rs'' : right_step' -> right_step''. Proof. intros RS' n; split; intros H1 m H2 H3. -apply lt_succ_r in H3; le_elim H3; -[now apply H1 | rewrite H3 in *; now apply RS']. -apply H1; [assumption | now apply lt_lt_succ_r]. +- apply lt_succ_r in H3; le_elim H3; + [now apply H1 | rewrite H3 in *; now apply RS']. +- apply H1; [assumption | now apply lt_lt_succ_r]. Qed. Lemma rbase : A' z. @@ -444,10 +447,12 @@ Theorem right_induction' : Proof. intros L R n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply L; now apply lt_le_incl. -apply L; now apply eq_le_incl. -apply right_induction. apply L; now apply eq_le_incl. assumption. -now apply lt_le_incl. +- apply L; now apply lt_le_incl. +- apply L; now apply eq_le_incl. +- apply right_induction. + + apply L; now apply eq_le_incl. + + assumption. + + now apply lt_le_incl. Qed. Theorem strong_right_induction' : @@ -455,9 +460,10 @@ Theorem strong_right_induction' : Proof. intros L R n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply L; now apply lt_le_incl. -apply L; now apply eq_le_incl. -apply strong_right_induction. assumption. now apply lt_le_incl. +- apply L; now apply lt_le_incl. +- apply L; now apply eq_le_incl. +- apply strong_right_induction. + + assumption. + now apply lt_le_incl. Qed. End RightInduction. @@ -472,17 +478,17 @@ Let left_step'' := forall n, A' n <-> A' (S n). Lemma ls_ls' : A z -> left_step -> left_step'. Proof. intros Az LS n H1 H2. le_elim H1. -apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl]. -rewrite H1; apply Az. +- apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl]. +- rewrite H1; apply Az. Qed. Lemma ls'_ls'' : left_step' -> left_step''. Proof. intros LS' n; split; intros H1 m H2 H3. -apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1. -le_elim H3. -apply le_succ_l in H3. now apply H1. -rewrite <- H3 in *; now apply LS'. +- apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1. +- le_elim H3. + + apply le_succ_l in H3. now apply H1. + + rewrite <- H3 in *; now apply LS'. Qed. Lemma lbase : A' (S z). @@ -512,10 +518,12 @@ Theorem left_induction' : Proof. intros R L n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply left_induction. apply R. now apply eq_le_incl. assumption. -now apply lt_le_incl. -rewrite H; apply R; now apply eq_le_incl. -apply R; now apply lt_le_incl. +- apply left_induction. + + apply R. now apply eq_le_incl. + + assumption. + + now apply lt_le_incl. +- rewrite H; apply R; now apply eq_le_incl. +- apply R; now apply lt_le_incl. Qed. Theorem strong_left_induction' : @@ -523,9 +531,9 @@ Theorem strong_left_induction' : Proof. intros R L n. destruct (lt_trichotomy n z) as [H | [H | H]]. -apply strong_left_induction; auto. now apply lt_le_incl. -rewrite H; apply R; now apply eq_le_incl. -apply R; now apply lt_le_incl. +- apply strong_left_induction; auto. now apply lt_le_incl. +- rewrite H; apply R; now apply eq_le_incl. +- apply R; now apply lt_le_incl. Qed. End LeftInduction. @@ -538,9 +546,9 @@ Theorem order_induction : Proof. intros Az RS LS n. destruct (lt_trichotomy n z) as [H | [H | H]]. -now apply left_induction; [| | apply lt_le_incl]. -now rewrite H. -now apply right_induction; [| | apply lt_le_incl]. +- now apply left_induction; [| | apply lt_le_incl]. +- now rewrite H. +- now apply right_induction; [| | apply lt_le_incl]. Qed. Theorem order_induction' : @@ -622,21 +630,24 @@ Theorem lt_wf : well_founded Rlt. Proof. unfold well_founded. apply strong_right_induction' with (z := z). -auto with typeclass_instances. -intros n H; constructor; intros y [H1 H2]. -apply nle_gt in H2. elim H2. now apply le_trans with z. -intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. +- auto with typeclass_instances. +- intros n H; constructor; intros y [H1 H2]. + apply nle_gt in H2. elim H2. now apply le_trans with z. +- intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. Qed. Theorem gt_wf : well_founded Rgt. Proof. unfold well_founded. apply strong_left_induction' with (z := z). -auto with typeclass_instances. -intros n H; constructor; intros y [H1 H2]. -apply nle_gt in H2. elim H2. now apply le_lt_trans with n. -intros n H1 H2; constructor; intros m [H3 H4]. -apply H2. assumption. now apply le_succ_l. +- auto with typeclass_instances. +- intros n H; constructor; intros y [H1 H2]. + apply nle_gt in H2. + + elim H2. + + now apply le_lt_trans with n. +- intros n H1 H2; constructor; intros m [H3 H4]. + apply H2. + + assumption. + now apply le_succ_l. Qed. End WF. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 93d99f08f5..84b8a96e64 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -48,20 +48,20 @@ Qed. Lemma Even_or_Odd : forall x, Even x \/ Odd x. Proof. nzinduct x. - left. exists 0. now nzsimpl. - intros x. - split; intros [(y,H)|(y,H)]. - right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl'. - right. - assert (LT : exists z, z<y). - destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x]. - rewrite <- le_succ_l, H. nzsimpl'. - rewrite <- (add_0_r y) at 3. now apply add_le_mono_l. - destruct LT as (z,LT). - destruct (lt_exists_pred z y LT) as (y' & Hy' & _). - exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'. - left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. + - left. exists 0. now nzsimpl. + - intros x. + split; intros [(y,H)|(y,H)]. + + right. exists y. rewrite H. now nzsimpl. + + left. exists (S y). rewrite H. now nzsimpl'. + + right. + assert (LT : exists z, z<y). + * destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x]. + rewrite <- le_succ_l, H. nzsimpl'. + rewrite <- (add_0_r y) at 3. now apply add_le_mono_l. + * destruct LT as (z,LT). + destruct (lt_exists_pred z y LT) as (y' & Hy' & _). + exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'. + + left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. Qed. Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1. @@ -80,16 +80,16 @@ Lemma Even_Odd_False : forall x, Even x -> Odd x -> False. Proof. intros x (y,E) (z,O). rewrite O in E; clear O. destruct (le_gt_cases y z) as [LE|GT]. -generalize (double_below _ _ LE); order. -generalize (double_above _ _ GT); order. +- generalize (double_below _ _ LE); order. +- generalize (double_above _ _ GT); order. Qed. Lemma orb_even_odd : forall n, orb (even n) (odd n) = true. Proof. intros. destruct (Even_or_Odd n) as [H|H]. - rewrite <- even_spec in H. now rewrite H. - rewrite <- odd_spec in H. now rewrite H, orb_true_r. + - rewrite <- even_spec in H. now rewrite H. + - rewrite <- odd_spec in H. now rewrite H, orb_true_r. Qed. Lemma negb_odd : forall n, negb (odd n) = even n. @@ -142,8 +142,8 @@ Qed. Lemma Odd_succ : forall n, Odd (S n) <-> Even n. Proof. split; intros (m,H). - exists m. apply succ_inj. now rewrite add_1_r in H. - exists m. rewrite add_1_r. now f_equiv. + - exists m. apply succ_inj. now rewrite add_1_r in H. + - exists m. rewrite add_1_r. now f_equiv. Qed. Lemma odd_succ : forall n, odd (S n) = even n. @@ -192,10 +192,10 @@ Proof. case_eq (even n); case_eq (even m); rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec; intros (m',Hm) (n',Hn). - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. + - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. + - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. + - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. + - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). @@ -210,14 +210,14 @@ Lemma even_mul : forall n m, even (mul n m) = even n || even m. Proof. intros. case_eq (even n); simpl; rewrite ?even_spec. - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. - case_eq (even m); simpl; rewrite ?even_spec. - intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2). - (* odd / odd *) - rewrite <- !negb_true_iff, !negb_even, !odd_spec. - intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m'). - rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r. - now rewrite add_shuffle1, add_assoc, !mul_assoc. + - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. + - case_eq (even m); simpl; rewrite ?even_spec. + + intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2). + (* odd / odd *) + + rewrite <- !negb_true_iff, !negb_even, !odd_spec. + intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m'). + rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r. + now rewrite add_shuffle1, add_assoc, !mul_assoc. Qed. Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index a1310667e1..830540bc66 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -60,8 +60,8 @@ Lemma pow_0_l' : forall a, a~=0 -> 0^a == 0. Proof. intros a Ha. destruct (lt_trichotomy a 0) as [LT|[EQ|GT]]; try order. - now rewrite pow_neg_r. - now apply pow_0_l. + - now rewrite pow_neg_r. + - now apply pow_0_l. Qed. Lemma pow_1_r : forall a, a^1 == a. @@ -71,9 +71,9 @@ Qed. Lemma pow_1_l : forall a, 0<=a -> 1^a == 1. Proof. - apply le_ind; intros. solve_proper. - now nzsimpl. - now nzsimpl. + apply le_ind; intros. - solve_proper. + - now nzsimpl. + - now nzsimpl. Qed. Hint Rewrite pow_1_r pow_1_l : nz. @@ -90,12 +90,12 @@ Hint Rewrite pow_2_r : nz. Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0. Proof. intros a b Hb. apply le_ind with (4:=Hb). - solve_proper. - rewrite pow_0_r. order'. - clear b Hb. intros b Hb IH. - rewrite pow_succ_r by trivial. - intros H. apply eq_mul_0 in H. destruct H; trivial. - now apply IH. + - solve_proper. + - rewrite pow_0_r. order'. + - clear b Hb. intros b Hb IH. + rewrite pow_succ_r by trivial. + intros H. apply eq_mul_0 in H. destruct H; trivial. + now apply IH. Qed. Lemma pow_nonzero : forall a b, a~=0 -> 0<=b -> a^b ~= 0. @@ -106,13 +106,13 @@ Qed. Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0<b /\ a==0). Proof. intros a b. split. - intros H. - destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]]. - now left. - rewrite Hb, pow_0_r in H; order'. - right. split; trivial. apply pow_eq_0 with b; order. - intros [Hb|[Hb Ha]]. now rewrite pow_neg_r. - rewrite Ha. apply pow_0_l'. order. + - intros H. + destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]]. + + now left. + + rewrite Hb, pow_0_r in H; order'. + + right. split; trivial. apply pow_eq_0 with b; order. + - intros [Hb|[Hb Ha]]. + now rewrite pow_neg_r. + + rewrite Ha. apply pow_0_l'. order. Qed. (** Power and addition, multiplication *) @@ -120,12 +120,12 @@ Qed. Lemma pow_add_r : forall a b c, 0<=b -> 0<=c -> a^(b+c) == a^b * a^c. Proof. - intros a b c Hb. apply le_ind with (4:=Hb). solve_proper. - now nzsimpl. - clear b Hb. intros b Hb IH Hc. - nzsimpl; trivial. - rewrite IH; trivial. apply mul_assoc. - now apply add_nonneg_nonneg. + intros a b c Hb. apply le_ind with (4:=Hb). - solve_proper. + - now nzsimpl. + - clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + + rewrite IH; trivial. apply mul_assoc. + + now apply add_nonneg_nonneg. Qed. Lemma pow_mul_l : forall a b c, @@ -133,23 +133,23 @@ Lemma pow_mul_l : forall a b c, Proof. intros a b c. destruct (lt_ge_cases c 0) as [Hc|Hc]. - rewrite !(pow_neg_r _ _ Hc). now nzsimpl. - apply le_ind with (4:=Hc). solve_proper. - now nzsimpl. - clear c Hc. intros c Hc IH. - nzsimpl; trivial. - rewrite IH; trivial. apply mul_shuffle1. + - rewrite !(pow_neg_r _ _ Hc). now nzsimpl. + - apply le_ind with (4:=Hc). + solve_proper. + + now nzsimpl. + + clear c Hc. intros c Hc IH. + nzsimpl; trivial. + rewrite IH; trivial. apply mul_shuffle1. Qed. Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c -> a^(b*c) == (a^b)^c. Proof. - intros a b c Hb. apply le_ind with (4:=Hb). solve_proper. - intros. now nzsimpl. - clear b Hb. intros b Hb IH Hc. - nzsimpl; trivial. - rewrite pow_add_r, IH, pow_mul_l; trivial. apply mul_comm. - now apply mul_nonneg_nonneg. + intros a b c Hb. apply le_ind with (4:=Hb). - solve_proper. + - intros. now nzsimpl. + - clear b Hb. intros b Hb IH Hc. + nzsimpl; trivial. + rewrite pow_add_r, IH, pow_mul_l; trivial. + apply mul_comm. + + now apply mul_nonneg_nonneg. Qed. (** Positivity *) @@ -158,67 +158,67 @@ Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b. Proof. intros a b Ha. destruct (lt_ge_cases b 0) as [Hb|Hb]. - now rewrite !(pow_neg_r _ _ Hb). - apply le_ind with (4:=Hb). solve_proper. - nzsimpl; order'. - clear b Hb. intros b Hb IH. - nzsimpl; trivial. now apply mul_nonneg_nonneg. + - now rewrite !(pow_neg_r _ _ Hb). + - apply le_ind with (4:=Hb). + solve_proper. + + nzsimpl; order'. + + clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_nonneg_nonneg. Qed. Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b. Proof. - intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper. - nzsimpl; order'. - clear b Hb. intros b Hb IH. - nzsimpl; trivial. now apply mul_pos_pos. + intros a b Ha Hb. apply le_ind with (4:=Hb). - solve_proper. + - nzsimpl; order'. + - clear b Hb. intros b Hb IH. + nzsimpl; trivial. now apply mul_pos_pos. Qed. (** Monotonicity *) Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c. Proof. - intros a b c Hc. apply lt_ind with (4:=Hc). solve_proper. - intros (Ha,H). nzsimpl; trivial; order. - clear c Hc. intros c Hc IH (Ha,H). - nzsimpl; try order. - apply mul_lt_mono_nonneg; trivial. - apply pow_nonneg; try order. - apply IH. now split. + intros a b c Hc. apply lt_ind with (4:=Hc). - solve_proper. + - intros (Ha,H). nzsimpl; trivial; order. + - clear c Hc. intros c Hc IH (Ha,H). + nzsimpl; try order. + apply mul_lt_mono_nonneg; trivial. + + apply pow_nonneg; try order. + + apply IH. now split. Qed. Lemma pow_le_mono_l : forall a b c, 0<=a<=b -> a^c <= b^c. Proof. intros a b c (Ha,H). destruct (lt_trichotomy c 0) as [Hc|[Hc|Hc]]. - rewrite !(pow_neg_r _ _ Hc); now nzsimpl. - rewrite Hc; now nzsimpl. - apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. - apply lt_le_incl, pow_lt_mono_l; now try split. + - rewrite !(pow_neg_r _ _ Hc); now nzsimpl. + - rewrite Hc; now nzsimpl. + - apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_l; now try split. Qed. Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b). Proof. intros a b Ha. split; intros Hb. - rewrite <- (pow_1_l b) by order. - apply pow_lt_mono_l; try split; order'. - destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial. - rewrite pow_neg_r in Hb; order'. - rewrite H, pow_0_r in Hb. order. + - rewrite <- (pow_1_l b) by order. + apply pow_lt_mono_l; try split; order'. + - destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial. + + rewrite pow_neg_r in Hb; order'. + + rewrite H, pow_0_r in Hb. order. Qed. Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=c -> b<c -> a^b < a^c. Proof. intros a b c Ha Hc H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'. - assert (H' : b<=c) by order. - destruct (le_exists_sub _ _ H') as (d & EQ & Hd). - rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1. - apply mul_lt_mono_pos_r. - apply pow_pos_nonneg; order'. - apply pow_gt_1; trivial. - apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial. - rewrite <- EQ' in *. rewrite add_0_l in EQ. order. + - rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'. + - assert (H' : b<=c) by order. + destruct (le_exists_sub _ _ H') as (d & EQ & Hd). + rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1. + apply mul_lt_mono_pos_r. + + apply pow_pos_nonneg; order'. + + apply pow_gt_1; trivial. + apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial. + rewrite <- EQ' in *. rewrite add_0_l in EQ. order. Qed. (** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *) @@ -227,20 +227,20 @@ Lemma pow_le_mono_r : forall a b c, 0<a -> b<=c -> a^b <= a^c. Proof. intros a b c Ha H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order. - apply le_succ_l in Ha; rewrite <- one_succ in Ha. - apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. - apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. - apply lt_le_incl, pow_lt_mono_r; order. - nzsimpl; order. + - rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order. + - apply le_succ_l in Ha; rewrite <- one_succ in Ha. + apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. + + apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. + apply lt_le_incl, pow_lt_mono_r; order. + + nzsimpl; order. Qed. Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d. Proof. intros. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. + - apply pow_le_mono_r; intuition order. + - apply pow_le_mono_l; intuition order. Qed. Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> @@ -249,10 +249,10 @@ Proof. intros a b c d (Ha,Hac) (Hb,Hbd). apply le_succ_l in Ha; rewrite <- one_succ in Ha. apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. - transitivity (a^d). - apply pow_lt_mono_r; intuition order. - apply pow_lt_mono_l; try split; order'. - nzsimpl; try order. apply pow_gt_1; order. + - transitivity (a^d). + + apply pow_lt_mono_r; intuition order. + + apply pow_lt_mono_l; try split; order'. + - nzsimpl; try order. apply pow_gt_1; order. Qed. (** Injectivity *) @@ -262,10 +262,10 @@ Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c -> Proof. intros a b c Ha Hb Hc EQ. destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial. - assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial). - order. - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). - order. + - assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial). + order. + - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. Qed. Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c -> @@ -273,10 +273,10 @@ Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c -> Proof. intros a b c Ha Hb Hc EQ. destruct (lt_trichotomy b c) as [LT|[EQ'|GT]]; trivial. - assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial). - order. - assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial). - order. + - assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial). + order. + - assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial). + order. Qed. (** Monotonicity results, both ways *) @@ -286,10 +286,10 @@ Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> Proof. intros a b c Ha Hb Hc. split; intro LT. - apply pow_lt_mono_l; try split; trivial. - destruct (le_gt_cases b a) as [LE|GT]; trivial. - assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order). - order. + - apply pow_lt_mono_l; try split; trivial. + - destruct (le_gt_cases b a) as [LE|GT]; trivial. + assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order). + order. Qed. Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> @@ -297,10 +297,10 @@ Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c -> Proof. intros a b c Ha Hb Hc. split; intro LE. - apply pow_le_mono_l; try split; trivial. - destruct (le_gt_cases a b) as [LE'|GT]; trivial. - assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). - order. + - apply pow_le_mono_l; try split; trivial. + - destruct (le_gt_cases a b) as [LE'|GT]; trivial. + assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial). + order. Qed. Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c -> @@ -308,10 +308,10 @@ Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c -> Proof. intros a b c Ha Hc. split; intro LT. - now apply pow_lt_mono_r. - destruct (le_gt_cases c b) as [LE|GT]; trivial. - assert (a^c <= a^b) by (apply pow_le_mono_r; order'). - order. + - now apply pow_lt_mono_r. + - destruct (le_gt_cases c b) as [LE|GT]; trivial. + assert (a^c <= a^b) by (apply pow_le_mono_r; order'). + order. Qed. Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c -> @@ -319,26 +319,26 @@ Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c -> Proof. intros a b c Ha Hc. split; intro LE. - apply pow_le_mono_r; order'. - destruct (le_gt_cases b c) as [LE'|GT]; trivial. - assert (a^c < a^b) by (apply pow_lt_mono_r; order'). - order. + - apply pow_le_mono_r; order'. + - destruct (le_gt_cases b c) as [LE'|GT]; trivial. + assert (a^c < a^b) by (apply pow_lt_mono_r; order'). + order. Qed. (** For any a>1, the a^x function is above the identity function *) Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b. Proof. - intros a b Ha Hb. apply le_ind with (4:=Hb). solve_proper. - nzsimpl. order'. - clear b Hb. intros b Hb IH. nzsimpl; trivial. - rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha. - transitivity (2*(S b)). - nzsimpl'. rewrite <- 2 succ_le_mono. - rewrite <- (add_0_l b) at 1. apply add_le_mono; order. - apply mul_le_mono_nonneg; trivial. - order'. - now apply lt_le_incl, lt_succ_r. + intros a b Ha Hb. apply le_ind with (4:=Hb). - solve_proper. + - nzsimpl. order'. + - clear b Hb. intros b Hb IH. nzsimpl; trivial. + rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha. + transitivity (2*(S b)). + + nzsimpl'. rewrite <- 2 succ_le_mono. + rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + + apply mul_le_mono_nonneg; trivial. + * order'. + * now apply lt_le_incl, lt_succ_r. Qed. (** Someday, we should say something about the full Newton formula. @@ -349,22 +349,22 @@ Qed. Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c -> a^c + b^c <= (a+b)^c. Proof. - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper. - nzsimpl; order. - clear c Hc. intros c Hc IH. - assert (0<=c) by order'. - nzsimpl; trivial. - transitivity ((a+b)*(a^c + b^c)). - rewrite mul_add_distr_r, !mul_add_distr_l. - apply add_le_mono. - rewrite <- add_0_r at 1. apply add_le_mono_l. - apply mul_nonneg_nonneg; trivial. - apply pow_nonneg; trivial. - rewrite <- add_0_l at 1. apply add_le_mono_r. - apply mul_nonneg_nonneg; trivial. - apply pow_nonneg; trivial. - apply mul_le_mono_nonneg_l; trivial. - now apply add_nonneg_nonneg. + intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). - solve_proper. + - nzsimpl; order. + - clear c Hc. intros c Hc IH. + assert (0<=c) by order'. + nzsimpl; trivial. + transitivity ((a+b)*(a^c + b^c)). + + rewrite mul_add_distr_r, !mul_add_distr_l. + apply add_le_mono. + * rewrite <- add_0_r at 1. apply add_le_mono_l. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg; trivial. + * rewrite <- add_0_l at 1. apply add_le_mono_r. + apply mul_nonneg_nonneg; trivial. + apply pow_nonneg; trivial. + + apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. Qed. (** This upper bound can also be seen as a convexity proof for x^c : @@ -377,37 +377,37 @@ Proof. assert (aux : forall a b c, 0<=a<=b -> 0<c -> (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)). (* begin *) - intros a b c (Ha,H) Hc. - rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. - rewrite <- !add_assoc. apply add_le_mono_l. - rewrite !add_assoc. apply add_le_mono_r. - destruct (le_exists_sub _ _ H) as (d & EQ & Hd). - rewrite EQ. - rewrite 2 mul_add_distr_r. - rewrite !add_assoc. apply add_le_mono_r. - rewrite add_comm. apply add_le_mono_l. - apply mul_le_mono_nonneg_l; trivial. - apply pow_le_mono_l; try split; order. - (* end *) - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_proper. - nzsimpl; order. - clear c Hc. intros c Hc IH. - assert (0<=c) by order. - nzsimpl; trivial. - transitivity ((a+b)*(2^(pred c) * (a^c + b^c))). - apply mul_le_mono_nonneg_l; trivial. - now apply add_nonneg_nonneg. - rewrite mul_assoc. rewrite (mul_comm (a+b)). - assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). - assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). - assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order). - rewrite EQ', <- !mul_assoc. - apply mul_le_mono_nonneg_l. - apply pow_nonneg; order'. - destruct (le_gt_cases a b). - apply aux; try split; order'. - rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). - apply aux; try split; order'. + - intros a b c (Ha,H) Hc. + rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. + rewrite <- !add_assoc. apply add_le_mono_l. + rewrite !add_assoc. apply add_le_mono_r. + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. + apply pow_le_mono_l; try split; order. + (* end *) + - intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). + solve_proper. + + nzsimpl; order. + + clear c Hc. intros c Hc IH. + assert (0<=c) by order. + nzsimpl; trivial. + transitivity ((a+b)*(2^(pred c) * (a^c + b^c))). + * apply mul_le_mono_nonneg_l; trivial. + now apply add_nonneg_nonneg. + * rewrite mul_assoc. rewrite (mul_comm (a+b)). + assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). + assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). + assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order). + rewrite EQ', <- !mul_assoc. + apply mul_le_mono_nonneg_l. + -- apply pow_nonneg; order'. + -- destruct (le_gt_cases a b). + ++ apply aux; try split; order'. + ++ rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). + apply aux; try split; order'. Qed. End NZPowProp. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index c2d2c4ae19..85ed71b8a4 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -49,18 +49,18 @@ Proof. intros b LT. destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso. assert ((S b)² < b²). - rewrite mul_succ_l, <- (add_0_r b²). - apply add_lt_le_mono. - apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r. - now apply le_succ_l. - order. + - rewrite mul_succ_l, <- (add_0_r b²). + apply add_lt_le_mono. + + apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r. + + now apply le_succ_l. + - order. Qed. Lemma sqrt_nonneg : forall a, 0<=√a. Proof. intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. - now rewrite (sqrt_neg _ Ha). - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. + - now rewrite (sqrt_neg _ Ha). + - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed. (** The spec of sqrt indeed determines it *) @@ -73,12 +73,12 @@ Proof. assert (Ha': 0<=√a) by now apply sqrt_nonneg. destruct (sqrt_spec a Ha) as (LEa,LTa). assert (b <= √a). - apply lt_succ_r, square_lt_simpl_nonneg; [|order]. - now apply lt_le_incl, lt_succ_r. - assert (√a <= b). - apply lt_succ_r, square_lt_simpl_nonneg; [|order]. - now apply lt_le_incl, lt_succ_r. - order. + - apply lt_succ_r, square_lt_simpl_nonneg; [|order]. + now apply lt_le_incl, lt_succ_r. + - assert (√a <= b). + + apply lt_succ_r, square_lt_simpl_nonneg; [|order]. + now apply lt_le_incl, lt_succ_r. + + order. Qed. (** Hence sqrt is a morphism *) @@ -87,9 +87,9 @@ Instance sqrt_wd : Proper (eq==>eq) sqrt. Proof. intros x x' Hx. destruct (lt_ge_cases x 0) as [H|H]. - rewrite 2 sqrt_neg; trivial. reflexivity. - now rewrite <- Hx. - apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec. + - rewrite 2 sqrt_neg; trivial. + reflexivity. + + now rewrite <- Hx. + - apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec. Qed. (** An alternate specification *) @@ -101,11 +101,11 @@ Proof. destruct (sqrt_spec _ Ha) as (LE,LT). destruct (le_exists_sub _ _ LE) as (r & Hr & Hr'). exists r. - split. now rewrite add_comm. - split. trivial. - apply (add_le_mono_r _ _ (√a)²). - rewrite <- Hr, add_comm. - generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc. + split. - now rewrite add_comm. + - split. + trivial. + + apply (add_le_mono_r _ _ (√a)²). + rewrite <- Hr, add_comm. + generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc. Qed. Lemma sqrt_unique' : forall a b c, 0<=c<=2*b -> @@ -115,10 +115,10 @@ Proof. apply sqrt_unique. rewrite EQ. split. - rewrite <- add_0_r at 1. now apply add_le_mono_l. - nzsimpl. apply lt_succ_r. - rewrite <- add_assoc. apply add_le_mono_l. - generalize H; now nzsimpl'. + - rewrite <- add_0_r at 1. now apply add_le_mono_l. + - nzsimpl. apply lt_succ_r. + rewrite <- add_assoc. apply add_le_mono_l. + generalize H; now nzsimpl'. Qed. (** Sqrt is exact on squares *) @@ -127,7 +127,7 @@ Lemma sqrt_square : forall a, 0<=a -> √(a²) == a. Proof. intros a Ha. apply sqrt_unique' with 0. - split. order. apply mul_nonneg_nonneg; order'. now nzsimpl. + - split. + order. + apply mul_nonneg_nonneg; order'. - now nzsimpl. Qed. (** Sqrt and predecessors of squares *) @@ -138,14 +138,14 @@ Proof. apply sqrt_unique. assert (EQ := lt_succ_pred 0 a Ha). rewrite EQ. split. - apply lt_succ_r. - rewrite (lt_succ_pred 0). - assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ). - assert (P a < a) by (now rewrite <- le_succ_l, EQ). - apply mul_lt_mono_nonneg; trivial. - now apply mul_pos_pos. - apply le_succ_l. - rewrite (lt_succ_pred 0). reflexivity. now apply mul_pos_pos. + - apply lt_succ_r. + rewrite (lt_succ_pred 0). + + assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ). + assert (P a < a) by (now rewrite <- le_succ_l, EQ). + apply mul_lt_mono_nonneg; trivial. + + now apply mul_pos_pos. + - apply le_succ_l. + rewrite (lt_succ_pred 0). + reflexivity. + now apply mul_pos_pos. Qed. (** Sqrt is a monotone function (but not a strict one) *) @@ -154,13 +154,13 @@ Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b. Proof. intros a b Hab. destruct (lt_ge_cases a 0) as [Ha|Ha]. - rewrite (sqrt_neg _ Ha). apply sqrt_nonneg. - assert (Hb : 0 <= b) by order. - destruct (sqrt_spec a Ha) as (LE,_). - destruct (sqrt_spec b Hb) as (_,LT). - apply lt_succ_r. - apply square_lt_simpl_nonneg; try order. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + - rewrite (sqrt_neg _ Ha). apply sqrt_nonneg. + - assert (Hb : 0 <= b) by order. + destruct (sqrt_spec a Ha) as (LE,_). + destruct (sqrt_spec b Hb) as (_,LT). + apply lt_succ_r. + apply square_lt_simpl_nonneg; try order. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. Qed. (** No reverse result for <=, consider for instance √2 <= √1 *) @@ -169,16 +169,16 @@ Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b. Proof. intros a b H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order. - destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|]. - destruct (sqrt_spec a Ha) as (_,LT). - destruct (sqrt_spec b Hb) as (LE,_). - apply le_succ_l in H. - assert ((S (√a))² <= (√b)²). - apply mul_le_mono_nonneg; trivial. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - order. + - rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order. + - destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|]. + destruct (sqrt_spec a Ha) as (_,LT). + destruct (sqrt_spec b Hb) as (LE,_). + apply le_succ_l in H. + assert ((S (√a))² <= (√b)²). + + apply mul_le_mono_nonneg; trivial. + * now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + * now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + + order. Qed. (** When left side is a square, we have an equivalence for <= *) @@ -186,11 +186,11 @@ Qed. Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= √a). Proof. intros a b Ha Hb. split; intros H. - rewrite <- (sqrt_square b); trivial. - now apply sqrt_le_mono. - destruct (sqrt_spec a Ha) as (LE,LT). - transitivity (√a)²; trivial. - now apply mul_le_mono_nonneg. + - rewrite <- (sqrt_square b); trivial. + now apply sqrt_le_mono. + - destruct (sqrt_spec a Ha) as (LE,LT). + transitivity (√a)²; trivial. + now apply mul_le_mono_nonneg. Qed. (** When right side is a square, we have an equivalence for < *) @@ -198,10 +198,10 @@ Qed. Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> √a < b). Proof. intros a b Ha Hb. split; intros H. - destruct (sqrt_spec a Ha) as (LE,_). - apply square_lt_simpl_nonneg; try order. - rewrite <- (sqrt_square b Hb) in H. - now apply sqrt_lt_cancel. + - destruct (sqrt_spec a Ha) as (LE,_). + apply square_lt_simpl_nonneg; try order. + - rewrite <- (sqrt_square b Hb) in H. + now apply sqrt_lt_cancel. Qed. (** Sqrt and basic constants *) @@ -218,14 +218,14 @@ Qed. Lemma sqrt_2 : √2 == 1. Proof. - apply sqrt_unique' with 1. nzsimpl; split; order'. now nzsimpl'. + apply sqrt_unique' with 1. - nzsimpl; split; order'. - now nzsimpl'. Qed. Lemma sqrt_pos : forall a, 0 < √a <-> 0 < a. Proof. - intros a. split; intros Ha. apply sqrt_lt_cancel. now rewrite sqrt_0. - rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono. - now rewrite one_succ, le_succ_l. + intros a. split; intros Ha. - apply sqrt_lt_cancel. now rewrite sqrt_0. + - rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono. + now rewrite one_succ, le_succ_l. Qed. Lemma sqrt_lt_lin : forall a, 1<a -> √a<a. @@ -239,11 +239,11 @@ Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a. Proof. intros a Ha. destruct (le_gt_cases a 0) as [H|H]. - setoid_replace a with 0 by order. now rewrite sqrt_0. - destruct (le_gt_cases a 1) as [H'|H']. - rewrite <- le_succ_l, <- one_succ in H. - setoid_replace a with 1 by order. now rewrite sqrt_1. - now apply lt_le_incl, sqrt_lt_lin. + - setoid_replace a with 0 by order. now rewrite sqrt_0. + - destruct (le_gt_cases a 1) as [H'|H']. + + rewrite <- le_succ_l, <- one_succ in H. + setoid_replace a with 1 by order. now rewrite sqrt_1. + + now apply lt_le_incl, sqrt_lt_lin. Qed. (** Sqrt and multiplication. *) @@ -255,28 +255,28 @@ Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b). Proof. intros a b. destruct (lt_ge_cases a 0) as [Ha|Ha]. - rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg. - assert (Ha':=sqrt_nonneg a). - assert (Hb':=sqrt_nonneg b). - apply sqrt_le_square; try now apply mul_nonneg_nonneg. - rewrite mul_shuffle1. - apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg. - now apply sqrt_spec. - now apply sqrt_spec. + - rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg. + - destruct (lt_ge_cases b 0) as [Hb|Hb]. + + rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg. + + assert (Ha':=sqrt_nonneg a). + assert (Hb':=sqrt_nonneg b). + apply sqrt_le_square; try now apply mul_nonneg_nonneg. + rewrite mul_shuffle1. + apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg. + * now apply sqrt_spec. + * now apply sqrt_spec. Qed. Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b). Proof. intros a b Ha Hb. apply sqrt_lt_square. - now apply mul_nonneg_nonneg. - apply mul_nonneg_nonneg. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - rewrite mul_shuffle1. - apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec. + - now apply mul_nonneg_nonneg. + - apply mul_nonneg_nonneg. + + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + - rewrite mul_shuffle1. + apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec. Qed. (** And we can't find better approximations in general. @@ -296,73 +296,73 @@ Proof. intros a Ha. apply lt_succ_r. apply sqrt_lt_square. - now apply le_le_succ_r. - apply le_le_succ_r, le_le_succ_r, sqrt_nonneg. - rewrite <- (add_1_l (S (√a))). - apply lt_le_trans with (1²+(S (√a))²). - rewrite mul_1_l, add_1_l, <- succ_lt_mono. - now apply sqrt_spec. - apply add_square_le. order'. apply le_le_succ_r, sqrt_nonneg. + - now apply le_le_succ_r. + - apply le_le_succ_r, le_le_succ_r, sqrt_nonneg. + - rewrite <- (add_1_l (S (√a))). + apply lt_le_trans with (1²+(S (√a))²). + + rewrite mul_1_l, add_1_l, <- succ_lt_mono. + now apply sqrt_spec. + + apply add_square_le. * order'. * apply le_le_succ_r, sqrt_nonneg. Qed. Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (√a) \/ √(S a) == √a. Proof. intros a Ha. destruct (le_gt_cases (√(S a)) (√a)) as [H|H]. - right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order. + - right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order. Qed. Lemma sqrt_eq_succ_iff_square : forall a, 0<=a -> (√(S a) == S (√a) <-> exists b, 0<b /\ S a == b²). Proof. intros a Ha. split. - intros EQ. exists (S (√a)). - split. apply lt_succ_r, sqrt_nonneg. - generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l. - assert (Ha' : 0 <= S a) by now apply le_le_succ_r. - generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order. - intros (b & Hb & H). - rewrite H. rewrite sqrt_square; try order. - symmetry. - rewrite <- (lt_succ_pred 0 b Hb). f_equiv. - rewrite <- (lt_succ_pred 0 b²) in H. apply succ_inj in H. - now rewrite H, sqrt_pred_square. - now apply mul_pos_pos. + - intros EQ. exists (S (√a)). + split. + apply lt_succ_r, sqrt_nonneg. + + generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l. + assert (Ha' : 0 <= S a) by now apply le_le_succ_r. + generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order. + - intros (b & Hb & H). + rewrite H. rewrite sqrt_square; try order. + symmetry. + rewrite <- (lt_succ_pred 0 b Hb). f_equiv. + rewrite <- (lt_succ_pred 0 b²) in H. + apply succ_inj in H. + now rewrite H, sqrt_pred_square. + + now apply mul_pos_pos. Qed. (** Sqrt and addition *) Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b. Proof. - assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b). - intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl. - apply sqrt_le_mono. - rewrite <- (add_0_l b) at 2. - apply add_le_mono_r; order. - intros a b. - destruct (lt_ge_cases a 0) as [Ha|Ha]. now apply AUX. - destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (add_comm a), (add_comm (√a)); now apply AUX. - assert (Ha':=sqrt_nonneg a). - assert (Hb':=sqrt_nonneg b). - rewrite <- lt_succ_r. - apply sqrt_lt_square. - now apply add_nonneg_nonneg. - now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg. - destruct (sqrt_spec a Ha) as (_,LTa). - destruct (sqrt_spec b Hb) as (_,LTb). - revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r. - intros LTa LTb. - assert (H:=add_le_mono _ _ _ _ LTa LTb). - etransitivity; [eexact H|]. clear LTa LTb H. - rewrite <- (add_assoc _ (√a) (√a)). - rewrite <- (add_assoc _ (√b) (√b)). - rewrite add_shuffle1. - rewrite <- (add_assoc _ (√a + √b)). - rewrite (add_shuffle1 (√a) (√b)). - apply add_le_mono_r. - now apply add_square_le. + assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b). + - intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl. + apply sqrt_le_mono. + rewrite <- (add_0_l b) at 2. + apply add_le_mono_r; order. + - intros a b. + destruct (lt_ge_cases a 0) as [Ha|Ha]. + now apply AUX. + + destruct (lt_ge_cases b 0) as [Hb|Hb]. + * rewrite (add_comm a), (add_comm (√a)); now apply AUX. + * assert (Ha':=sqrt_nonneg a). + assert (Hb':=sqrt_nonneg b). + rewrite <- lt_succ_r. + apply sqrt_lt_square. + -- now apply add_nonneg_nonneg. + -- now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg. + -- destruct (sqrt_spec a Ha) as (_,LTa). + destruct (sqrt_spec b Hb) as (_,LTb). + revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r. + intros LTa LTb. + assert (H:=add_le_mono _ _ _ _ LTa LTb). + etransitivity; [eexact H|]. clear LTa LTb H. + rewrite <- (add_assoc _ (√a) (√a)). + rewrite <- (add_assoc _ (√b) (√b)). + rewrite add_shuffle1. + rewrite <- (add_assoc _ (√a + √b)). + rewrite (add_shuffle1 (√a) (√b)). + apply add_le_mono_r. + now apply add_square_le. Qed. (** convexity inequality for sqrt: sqrt of middle is above middle @@ -374,12 +374,12 @@ Proof. assert (Ha':=sqrt_nonneg a). assert (Hb':=sqrt_nonneg b). apply sqrt_le_square. - apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg. - now apply add_nonneg_nonneg. - transitivity (2*((√a)² + (√b)²)). - now apply square_add_le. - apply mul_le_mono_nonneg_l. order'. - apply add_le_mono; now apply sqrt_spec. + - apply mul_nonneg_nonneg. + order'. + now apply add_nonneg_nonneg. + - now apply add_nonneg_nonneg. + - transitivity (2*((√a)² + (√b)²)). + + now apply square_add_le. + + apply mul_le_mono_nonneg_l. * order'. + * apply add_le_mono; now apply sqrt_spec. Qed. End NZSqrtProp. @@ -430,8 +430,8 @@ Qed. Lemma sqrt_up_nonneg : forall a, 0<=√°a. Proof. intros. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite sqrt_up_eqn0. - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. + - now rewrite sqrt_up_eqn0. + - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. Qed. (** [sqrt_up] is a morphism *) @@ -439,8 +439,8 @@ Qed. Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up. Proof. assert (Proper (eq==>eq==>Logic.eq) compare). - intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. - intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx. + - intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. + - intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx. Qed. (** The spec of [sqrt_up] indeed determines it *) @@ -463,9 +463,9 @@ Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a. Proof. intros a Ha. le_elim Ha. - rewrite sqrt_up_eqn by (now apply mul_pos_pos). - rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial. - rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl. + - rewrite sqrt_up_eqn by (now apply mul_pos_pos). + rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial. + - rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl. Qed. (** [sqrt_up] and successors of squares *) @@ -500,10 +500,10 @@ Qed. Lemma le_sqrt_sqrt_up : forall a, √a <= √°a. Proof. intros a. unfold sqrt_up. case compare_spec; intros H. - rewrite <- H, sqrt_0. order. - rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le. - apply lt_succ_r. now rewrite (lt_succ_pred 0 a H). - now rewrite sqrt_neg. + - rewrite <- H, sqrt_0. order. + - rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le. + apply lt_succ_r. now rewrite (lt_succ_pred 0 a H). + - now rewrite sqrt_neg. Qed. Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a). @@ -517,21 +517,21 @@ Qed. Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)². Proof. intros a H. split. - now apply sqrt_spec. - le_elim H. - now apply sqrt_up_spec. - now rewrite <-H, sqrt_up_0, mul_0_l. + - now apply sqrt_spec. + - le_elim H. + + now apply sqrt_up_spec. + + now rewrite <-H, sqrt_up_0, mul_0_l. Qed. Lemma sqrt_sqrt_up_exact : forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. - split. intros. exists √a. - split. apply sqrt_nonneg. - generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b & Hb & Hb'). rewrite Hb'. - now rewrite sqrt_square, sqrt_up_square. + split. - intros. exists √a. + split. + apply sqrt_nonneg. + + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. + - intros (b & Hb & Hb'). rewrite Hb'. + now rewrite sqrt_square, sqrt_up_square. Qed. (** [sqrt_up] is a monotone function (but not a strict one) *) @@ -540,9 +540,9 @@ Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b. Proof. intros a b H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg. - rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono. - apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order. + - rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg. + - rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono. + apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order. Qed. (** No reverse result for <=, consider for instance √°3 <= √°2 *) @@ -551,10 +551,10 @@ Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b. Proof. intros a b H. destruct (le_gt_cases b 0) as [Hb|Hb]. - rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order. - destruct (le_gt_cases a 0) as [Ha|Ha]; [order|]. - rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono. - apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn. + - rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order. + - destruct (le_gt_cases a 0) as [Ha|Ha]; [order|]. + rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono. + apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn. Qed. (** When left side is a square, we have an equivalence for < *) @@ -562,10 +562,10 @@ Qed. Lemma sqrt_up_lt_square : forall a b, 0<=a -> 0<=b -> (b² < a <-> b < √°a). Proof. intros a b Ha Hb. split; intros H. - destruct (sqrt_up_spec a) as (LE,LT). - apply le_lt_trans with b²; trivial using square_nonneg. - apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg. - apply sqrt_up_lt_cancel. now rewrite sqrt_up_square. + - destruct (sqrt_up_spec a) as (LE,LT). + + apply le_lt_trans with b²; trivial using square_nonneg. + + apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg. + - apply sqrt_up_lt_cancel. now rewrite sqrt_up_square. Qed. (** When right side is a square, we have an equivalence for <= *) @@ -573,17 +573,17 @@ Qed. Lemma sqrt_up_le_square : forall a b, 0<=a -> 0<=b -> (a <= b² <-> √°a <= b). Proof. intros a b Ha Hb. split; intros H. - rewrite <- (sqrt_up_square b Hb). - now apply sqrt_up_le_mono. - apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg]. - transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec. + - rewrite <- (sqrt_up_square b Hb). + now apply sqrt_up_le_mono. + - apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg]. + transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec. Qed. Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a. Proof. - intros a. split; intros Ha. apply sqrt_up_lt_cancel. now rewrite sqrt_up_0. - rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono. - now rewrite one_succ, le_succ_l. + intros a. split; intros Ha. - apply sqrt_up_lt_cancel. now rewrite sqrt_up_0. + - rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono. + now rewrite one_succ, le_succ_l. Qed. Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a. @@ -599,11 +599,11 @@ Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a. Proof. intros a Ha. le_elim Ha. - rewrite sqrt_up_eqn; trivial. apply le_succ_l. - apply le_lt_trans with (P a). apply sqrt_le_lin. - now rewrite <- lt_succ_r, (lt_succ_pred 0). - rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r. - now rewrite <- Ha, sqrt_up_0. + - rewrite sqrt_up_eqn; trivial. apply le_succ_l. + apply le_lt_trans with (P a). + apply sqrt_le_lin. + now rewrite <- lt_succ_r, (lt_succ_pred 0). + + rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r. + - now rewrite <- Ha, sqrt_up_0. Qed. (** [sqrt_up] and multiplication. *) @@ -615,23 +615,23 @@ Lemma sqrt_up_mul_above : forall a b, 0<=a -> 0<=b -> √°(a*b) <= √°a * √ Proof. intros a b Ha Hb. apply sqrt_up_le_square. - now apply mul_nonneg_nonneg. - apply mul_nonneg_nonneg; apply sqrt_up_nonneg. - rewrite mul_shuffle1. - apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec. + - now apply mul_nonneg_nonneg. + - apply mul_nonneg_nonneg; apply sqrt_up_nonneg. + - rewrite mul_shuffle1. + apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec. Qed. Lemma sqrt_up_mul_below : forall a b, 0<a -> 0<b -> (P √°a)*(P √°b) < √°(a*b). Proof. intros a b Ha Hb. apply sqrt_up_lt_square. - apply mul_nonneg_nonneg; order. - apply mul_nonneg_nonneg; apply lt_succ_r. - rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. - rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. - rewrite mul_shuffle1. - apply mul_lt_mono_nonneg; trivial using square_nonneg; - now apply sqrt_up_spec. + - apply mul_nonneg_nonneg; order. + - apply mul_nonneg_nonneg; apply lt_succ_r. + + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. + + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. + - rewrite mul_shuffle1. + apply mul_lt_mono_nonneg; trivial using square_nonneg; + now apply sqrt_up_spec. Qed. (** And we can't find better approximations in general. @@ -650,37 +650,37 @@ Lemma sqrt_up_succ_le : forall a, 0<=a -> √°(S a) <= S (√°a). Proof. intros a Ha. apply sqrt_up_le_square. - now apply le_le_succ_r. - apply le_le_succ_r, sqrt_up_nonneg. - rewrite <- (add_1_l (√°a)). - apply le_trans with (1²+(√°a)²). - rewrite mul_1_l, add_1_l, <- succ_le_mono. - now apply sqrt_sqrt_up_spec. - apply add_square_le. order'. apply sqrt_up_nonneg. + - now apply le_le_succ_r. + - apply le_le_succ_r, sqrt_up_nonneg. + - rewrite <- (add_1_l (√°a)). + apply le_trans with (1²+(√°a)²). + + rewrite mul_1_l, add_1_l, <- succ_le_mono. + now apply sqrt_sqrt_up_spec. + + apply add_square_le. * order'. * apply sqrt_up_nonneg. Qed. Lemma sqrt_up_succ_or : forall a, 0<=a -> √°(S a) == S (√°a) \/ √°(S a) == √°a. Proof. intros a Ha. destruct (le_gt_cases (√°(S a)) (√°a)) as [H|H]. - right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order. + - right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order. + - left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order. Qed. Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a -> (√°(S a) == S (√°a) <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. split. - intros EQ. - le_elim Ha. - exists (√°a). split. apply sqrt_up_nonneg. - generalize (proj2 (sqrt_up_spec a Ha)). - assert (Ha' : 0 < S a) by (apply lt_succ_r; order'). - generalize (proj1 (sqrt_up_spec (S a) Ha')). - rewrite EQ, pred_succ, lt_succ_r. order. - exists 0. nzsimpl. now split. - intros (b & Hb & H). - now rewrite H, sqrt_up_succ_square, sqrt_up_square. + - intros EQ. + le_elim Ha. + + exists (√°a). split. * apply sqrt_up_nonneg. + * generalize (proj2 (sqrt_up_spec a Ha)). + assert (Ha' : 0 < S a) by (apply lt_succ_r; order'). + generalize (proj1 (sqrt_up_spec (S a) Ha')). + rewrite EQ, pred_succ, lt_succ_r. order. + + exists 0. nzsimpl. now split. + - intros (b & Hb & H). + now rewrite H, sqrt_up_succ_square, sqrt_up_square. Qed. (** [sqrt_up] and addition *) @@ -688,21 +688,21 @@ Qed. Lemma sqrt_up_add_le : forall a b, √°(a+b) <= √°a + √°b. Proof. assert (AUX : forall a b, a<=0 -> √°(a+b) <= √°a + √°b). - intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl. - apply sqrt_up_le_mono. - rewrite <- (add_0_l b) at 2. - apply add_le_mono_r; order. - intros a b. - destruct (le_gt_cases a 0) as [Ha|Ha]. now apply AUX. - destruct (le_gt_cases b 0) as [Hb|Hb]. - rewrite (add_comm a), (add_comm (√°a)); now apply AUX. - rewrite 2 sqrt_up_eqn; trivial. - nzsimpl. rewrite <- succ_le_mono. - transitivity (√(P a) + √b). - rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le. - apply add_le_mono_l. - apply le_sqrt_sqrt_up. - now apply add_pos_pos. + - intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl. + apply sqrt_up_le_mono. + rewrite <- (add_0_l b) at 2. + apply add_le_mono_r; order. + - intros a b. + destruct (le_gt_cases a 0) as [Ha|Ha]. + now apply AUX. + + destruct (le_gt_cases b 0) as [Hb|Hb]. + * rewrite (add_comm a), (add_comm (√°a)); now apply AUX. + * rewrite 2 sqrt_up_eqn; trivial. + -- nzsimpl. rewrite <- succ_le_mono. + transitivity (√(P a) + √b). + ++ rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le. + ++ apply add_le_mono_l. + apply le_sqrt_sqrt_up. + -- now apply add_pos_pos. Qed. (** Convexity-like inequality for [sqrt_up]: [sqrt_up] of middle is above middle @@ -712,25 +712,24 @@ Qed. Lemma add_sqrt_up_le : forall a b, 0<=a -> 0<=b -> √°a + √°b <= S √°(2*(a+b)). Proof. intros a b Ha Hb. - le_elim Ha. - le_elim Hb. - rewrite 3 sqrt_up_eqn; trivial. - nzsimpl. rewrite <- 2 succ_le_mono. - etransitivity; [eapply add_sqrt_le|]. - apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha). - apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb). - apply sqrt_le_mono. - apply lt_succ_r. rewrite (lt_succ_pred 0). - apply mul_lt_mono_pos_l. order'. - apply add_lt_mono. - apply le_succ_l. now rewrite (lt_succ_pred 0). - apply le_succ_l. now rewrite (lt_succ_pred 0). - apply mul_pos_pos. order'. now apply add_pos_pos. - apply mul_pos_pos. order'. now apply add_pos_pos. - rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. - rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'. - rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. - rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'. + le_elim Ha;[le_elim Hb|]. + - rewrite 3 sqrt_up_eqn; trivial. + + nzsimpl. rewrite <- 2 succ_le_mono. + etransitivity; [eapply add_sqrt_le|]. + * apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha). + * apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb). + * apply sqrt_le_mono. + apply lt_succ_r. rewrite (lt_succ_pred 0). + -- apply mul_lt_mono_pos_l. ++ order'. + ++ apply add_lt_mono. + ** apply le_succ_l. now rewrite (lt_succ_pred 0). + ** apply le_succ_l. now rewrite (lt_succ_pred 0). + -- apply mul_pos_pos. ++ order'. ++ now apply add_pos_pos. + + apply mul_pos_pos. * order'. * now apply add_pos_pos. + - rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. + rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'. + - rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. + rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'. Qed. End NZSqrtUpProp. |