From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- theories/Numbers/NatInt/NZAdd.v | 34 +- theories/Numbers/NatInt/NZAddOrder.v | 35 +- theories/Numbers/NatInt/NZAxioms.v | 42 +- theories/Numbers/NatInt/NZBase.v | 19 +- theories/Numbers/NatInt/NZBits.v | 64 +++ theories/Numbers/NatInt/NZDiv.v | 112 +++-- theories/Numbers/NatInt/NZDomain.v | 121 ++--- theories/Numbers/NatInt/NZGcd.v | 307 ++++++++++++ theories/Numbers/NatInt/NZLog.v | 889 +++++++++++++++++++++++++++++++++ theories/Numbers/NatInt/NZMul.v | 37 +- theories/Numbers/NatInt/NZMulOrder.v | 221 +++++--- theories/Numbers/NatInt/NZOrder.v | 129 ++--- theories/Numbers/NatInt/NZParity.v | 263 ++++++++++ theories/Numbers/NatInt/NZPow.v | 411 +++++++++++++++ theories/Numbers/NatInt/NZProperties.v | 8 +- theories/Numbers/NatInt/NZSqrt.v | 734 +++++++++++++++++++++++++++ 16 files changed, 3106 insertions(+), 320 deletions(-) create mode 100644 theories/Numbers/NatInt/NZBits.v create mode 100644 theories/Numbers/NatInt/NZGcd.v create mode 100644 theories/Numbers/NatInt/NZLog.v create mode 100644 theories/Numbers/NatInt/NZParity.v create mode 100644 theories/Numbers/NatInt/NZPow.v create mode 100644 theories/Numbers/NatInt/NZSqrt.v (limited to 'theories/Numbers/NatInt') diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 782619f0..8bed3027 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* p + n < p + m. Proof. @@ -30,7 +28,7 @@ Theorem add_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q. Proof. intros n m p q H1 H2. apply lt_trans with (m + p); -[now apply -> add_lt_mono_r | now apply -> add_lt_mono_l]. +[now apply add_lt_mono_r | now apply add_lt_mono_l]. Qed. Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m. @@ -48,21 +46,21 @@ Theorem add_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q. Proof. intros n m p q H1 H2. apply le_trans with (m + p); -[now apply -> add_le_mono_r | now apply -> add_le_mono_l]. +[now apply add_le_mono_r | now apply add_le_mono_l]. Qed. Theorem add_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q. Proof. intros n m p q H1 H2. apply lt_le_trans with (m + p); -[now apply -> add_lt_mono_r | now apply -> add_le_mono_l]. +[now apply add_lt_mono_r | now apply add_le_mono_l]. Qed. Theorem add_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q. Proof. intros n m p q H1 H2. apply le_lt_trans with (m + p); -[now apply -> add_le_mono_r | now apply -> add_lt_mono_l]. +[now apply add_le_mono_r | now apply add_lt_mono_l]. Qed. Theorem add_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n + m. @@ -149,5 +147,22 @@ Proof. intros n m H; apply add_le_cases; now nzsimpl. Qed. -End NZAddOrderPropSig. +(** Substraction *) + +(** We can prove the existence of a subtraction of any number by + a smaller one *) + +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. +Qed. + +(** For the moment, it doesn't seem possible to relate + this existing subtraction with [sub]. +*) + +End NZAddOrderProp. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 33236cde..fcd98787 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* t. End ZeroSuccPred. @@ -28,8 +26,6 @@ Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T). Notation "0" := zero. Notation S := succ. Notation P := pred. - Notation "1" := (S 0). - Notation "2" := (S 1). End ZeroSuccPredNotation. Module Type ZeroSuccPred' (T:Typ) := @@ -44,9 +40,33 @@ Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E). A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n. End IsNZDomain. -Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain. -Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain. +(** Axiomatization of some more constants + + Simply denoting "1" for (S 0) and so on works ok when implementing + by nat, but leaves some (Nsucc N0) when implementing by N. +*) + +Module Type OneTwo (Import T:Typ). + Parameter Inline(20) one two : t. +End OneTwo. +Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T). + Notation "1" := one. + Notation "2" := two. +End OneTwoNotation. + +Module Type OneTwo' (T:Typ) := OneTwo T <+ OneTwoNotation T. + +Module Type IsOneTwo (E:Eq')(Z:ZeroSuccPred' E)(O:OneTwo' E). + Import E Z O. + Axiom one_succ : 1 == S 0. + Axiom two_succ : 2 == S 1. +End IsOneTwo. + +Module Type NZDomainSig := + EqualityType <+ ZeroSuccPred <+ IsNZDomain <+ OneTwo <+ IsOneTwo. +Module Type NZDomainSig' := + EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo. (** Axiomatization of basic operations : [+] [-] [*] *) @@ -117,3 +137,9 @@ Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare. Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare. Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare. +(** A square function *) + +Module Type NZSquare (Import NZ : NZBasicFunsSig'). + Parameter Inline square : t -> t. + Axiom square_spec : forall n, square n == n * n. +End NZSquare. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 119f8265..65b64635 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* n1 == n2. Proof. intros; split. apply succ_inj. -apply succ_wd. +intros. now f_equiv. Qed. Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m. @@ -63,7 +66,7 @@ left-inverse to the successor at this point *) Section CentralInduction. -Variable A : predicate t. +Variable A : t -> Prop. Hypothesis A_wd : Proper (eq==>iff) A. Theorem central_induction : @@ -72,7 +75,7 @@ Theorem central_induction : forall n, A n. Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. -solve_predicate_wd. +solve_proper. intro; now apply bi_induction. intro; pose proof (Step n); tauto. Qed. @@ -85,5 +88,5 @@ Tactic Notation "nzinduct" ident(n) := Tactic Notation "nzinduct" ident(n) constr(u) := induction_maker n ltac:(apply central_induction with (z := u)). -End NZBasePropSig. +End NZBaseProp. diff --git a/theories/Numbers/NatInt/NZBits.v b/theories/Numbers/NatInt/NZBits.v new file mode 100644 index 00000000..dc97eeb1 --- /dev/null +++ b/theories/Numbers/NatInt/NZBits.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> bool. + Parameters Inline shiftl shiftr land lor ldiff lxor : t -> t -> t. + Parameter Inline div2 : t -> t. +End Bits. + +Module Type BitsNotation (Import A : Typ)(Import B : Bits A). + Notation "a .[ n ]" := (testbit a n) (at level 5, format "a .[ n ]"). + Infix ">>" := shiftr (at level 30, no associativity). + Infix "<<" := shiftl (at level 30, no associativity). +End BitsNotation. + +Module Type Bits' (A:Typ) := Bits A <+ BitsNotation A. + +Module Type NZBitsSpec + (Import A : NZOrdAxiomsSig')(Import B : Bits' A). + + Declare Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. + Axiom testbit_odd_0 : forall a, (2*a+1).[0] = true. + Axiom testbit_even_0 : forall a, (2*a).[0] = false. + Axiom testbit_odd_succ : forall a n, 0<=n -> (2*a+1).[S n] = a.[n]. + Axiom testbit_even_succ : forall a n, 0<=n -> (2*a).[S n] = a.[n]. + Axiom testbit_neg_r : forall a n, n<0 -> a.[n] = false. + + Axiom shiftr_spec : forall a n m, 0<=m -> (a >> n).[m] = a.[m+n]. + Axiom shiftl_spec_high : forall a n m, 0<=m -> n<=m -> (a << n).[m] = a.[m-n]. + Axiom shiftl_spec_low : forall a n m, m (a << n).[m] = false. + + Axiom land_spec : forall a b n, (land a b).[n] = a.[n] && b.[n]. + Axiom lor_spec : forall a b n, (lor a b).[n] = a.[n] || b.[n]. + Axiom ldiff_spec : forall a b n, (ldiff a b).[n] = a.[n] && negb b.[n]. + Axiom lxor_spec : forall a b n, (lxor a b).[n] = xorb a.[n] b.[n]. + Axiom div2_spec : forall a, div2 a == a >> 1. + +End NZBitsSpec. + +Module Type NZBits (A:NZOrdAxiomsSig) := Bits A <+ NZBitsSpec A. +Module Type NZBits' (A:NZOrdAxiomsSig) := Bits' A <+ NZBitsSpec A. + +(** In the functor of properties will also be defined: + - [setbit : t -> t -> t ] defined as [lor a (1< t -> t ] defined as [ldiff a (1< t], the number with [n] initial true bits, + corresponding to [2^n - 1]. + - a logical complement [lnot]. For integer numbers it will + be a [t->t], doing a swap of all bits, while on natural + numbers, it will be a bounded complement [t->t->t], swapping + only the first [n] bits. +*) + +(** For the moment, no shared properties about NZ here, + since properties and proofs for N and Z are quite different *) diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index ba1c171e..bc109ace 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* t -> t. End DivMod. -Module Type DivModNotation (T:Typ)(Import NZ:DivMod T). +Module Type DivModNotation (A : Typ)(Import B : DivMod A). Infix "/" := div. Infix "mod" := modulo (at level 40, no associativity). End DivModNotation. -Module Type DivMod' (T:Typ) := DivMod T <+ DivModNotation T. +Module Type DivMod' (A : Typ) := DivMod A <+ DivModNotation A. -Module Type NZDivCommon (Import NZ : NZAxiomsSig')(Import DM : DivMod' NZ). +Module Type NZDivSpec (Import A : NZOrdAxiomsSig')(Import B : DivMod' A). Declare Instance div_wd : Proper (eq==>eq==>eq) div. Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo. Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b). -End NZDivCommon. + Axiom mod_bound_pos : forall a b, 0<=a -> 0 0 <= a mod b < b. +End NZDivSpec. (** The different divisions will only differ in the conditions - they impose on [modulo]. For NZ, we only describe behavior - on positive numbers. - - NB: This axiom would also be true for N and Z, but redundant. + they impose on [modulo]. For NZ, we have only described the + behavior on positive numbers. *) -Module Type NZDivSpecific (Import NZ : NZOrdAxiomsSig')(Import DM : DivMod' NZ). - Axiom mod_bound : forall a b, 0<=a -> 0 0 <= a mod b < b. -End NZDivSpecific. - -Module Type NZDiv (NZ:NZOrdAxiomsSig) - := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ. +Module Type NZDiv (A : NZOrdAxiomsSig) := DivMod A <+ NZDivSpec A. +Module Type NZDiv' (A : NZOrdAxiomsSig) := NZDiv A <+ DivModNotation A. -Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ. - -Module NZDivPropFunct - (Import NZ : NZOrdAxiomsSig') - (Import NZP : NZMulOrderPropSig NZ) - (Import NZD : NZDiv' NZ) -. +Module Type NZDivProp + (Import A : NZOrdAxiomsSig') + (Import B : NZDiv' A) + (Import C : NZMulOrderProp A). (** Uniqueness theorems *) @@ -84,7 +76,7 @@ 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; order. +apply mod_bound_pos; order. rewrite <- div_mod; order. Qed. @@ -94,18 +86,21 @@ 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; order. +apply mod_bound_pos; order. rewrite <- div_mod; order. Qed. +Theorem div_unique_exact a b q: + 0<=a -> 0 a == b*q -> q == a/b. +Proof. + intros Ha Hb H. apply div_unique with 0; nzsimpl; now try split. +Qed. (** A division by itself returns 1 *) Lemma div_same : forall a, 0 a/a == 1. Proof. -intros. symmetry. -apply div_unique with 0; intuition; try order. -now nzsimpl. +intros. symmetry. apply div_unique_exact; nzsimpl; order. Qed. Lemma mod_same : forall a, 0 a mod a == 0. @@ -147,9 +142,7 @@ Qed. Lemma div_1_r: forall a, 0<=a -> a/1 == a. Proof. -intros. symmetry. -apply div_unique with 0; try split; try order; try apply lt_0_1. -now nzsimpl. +intros. symmetry. apply div_unique_exact; nzsimpl; order'. Qed. Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0. @@ -161,20 +154,19 @@ Qed. Lemma div_1_l: forall a, 1 1/a == 0. Proof. -intros; apply div_small; split; auto. apply le_succ_diag_r. +intros; apply div_small; split; auto. apply le_0_1. Qed. Lemma mod_1_l: forall a, 1 1 mod a == 1. Proof. -intros; apply mod_small; split; auto. apply le_succ_diag_r. +intros; apply mod_small; split; auto. apply le_0_1. Qed. Lemma div_mul : forall a b, 0<=a -> 0 (a*b)/b == a. Proof. -intros; symmetry. -apply div_unique with 0; try split; try order. +intros; symmetry. apply div_unique_exact; trivial. apply mul_nonneg_nonneg; order. -nzsimpl; apply mul_comm. +apply mul_comm. Qed. Lemma mod_mul : forall a b, 0<=a -> 0 (a*b) mod b == 0. @@ -194,7 +186,7 @@ Theorem mod_le: forall a b, 0<=a -> 0 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 a b); auto. +apply lt_le_incl. destruct (mod_bound_pos a b); auto. rewrite lt_eq_cases; right. apply mod_small; auto. Qed. @@ -216,7 +208,7 @@ Lemma div_str_pos : forall a b, 0 0 < a/b. Proof. intros a b (Hb,Hab). assert (LE : 0 <= a/b) by (apply div_pos; order). -assert (MOD : a mod b < b) by (destruct (mod_bound a b); order). +assert (MOD : a mod b < b) by (destruct (mod_bound_pos a b); order). rewrite lt_eq_cases in LE; destruct LE as [LT|EQ]; auto. exfalso; revert Hab. rewrite (div_mod a b), <-EQ; nzsimpl; order. @@ -263,7 +255,7 @@ 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 a b); order. +rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed. (** [le] is compatible with a positive division. *) @@ -282,8 +274,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 b c); order. -rewrite <- add_le_mono_l. destruct (mod_bound 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 *) @@ -293,7 +285,7 @@ Proof. intros. rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order. rewrite <- (add_0_r a) at 1. -rewrite <- add_le_mono_l. destruct (mod_bound a b); order. +rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed. Lemma mul_succ_div_gt : forall a b, 0<=a -> 0 a < b*(S (a/b)). @@ -302,7 +294,7 @@ intros. rewrite (div_mod a b) at 1 by order. rewrite (mul_succ_r). rewrite <- add_lt_mono_l. -destruct (mod_bound a b); auto. +destruct (mod_bound_pos a b); auto. Qed. @@ -359,7 +351,7 @@ Proof. 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 p r); order. + rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order. Qed. @@ -371,7 +363,7 @@ Proof. intros. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound; auto. + apply mod_bound_pos; auto. rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order. now rewrite mul_comm. Qed. @@ -404,8 +396,8 @@ Proof. apply div_unique with ((a mod b)*c). apply mul_nonneg_nonneg; order. split. - apply mul_nonneg_nonneg; destruct (mod_bound a b); order. - rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound a b); auto. + 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. @@ -441,7 +433,7 @@ Qed. Theorem mod_mod: forall a n, 0<=a -> 0 (a mod n) mod n == a mod n. Proof. - intros. destruct (mod_bound a n); auto. now rewrite mod_small_iff. + intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. Qed. Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0 @@ -454,7 +446,7 @@ Proof. rewrite mul_add_distr_l, mul_assoc. intros. rewrite mod_add; auto. now rewrite mul_comm. - apply mul_nonneg_nonneg; destruct (mod_bound a n); auto. + 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 @@ -467,7 +459,7 @@ Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0 (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 b n). + now destruct (mod_bound_pos b n). Qed. Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0 @@ -478,7 +470,7 @@ Proof. 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 a n); auto. + 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 @@ -491,7 +483,7 @@ Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0 (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 b n). + now destruct (mod_bound_pos b n). Qed. Lemma div_div : forall a b c, 0<=a -> 0 0 @@ -500,7 +492,7 @@ Proof. intros a b c Ha Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b); trivial. (* begin 0<= ... 0 0 + a mod (b*c) == a mod b + b*((a/b) mod c). +Proof. + intros a b c Ha Hb Hc. + apply add_cancel_l with (b*c*(a/(b*c))). + rewrite <- div_mod by (apply neq_mul_0; split; order). + rewrite <- div_div by trivial. + rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l. + rewrite <- div_mod by order. + apply div_mod; order. +Qed. + (** A last inequality: *) Theorem div_mul_le: @@ -538,5 +542,5 @@ Proof. rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. Qed. -End NZDivPropFunct. +End NZDivProp. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 9dba3c3c..36aaa3e7 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* A)(n:nat) : A -> A := fun a => - match n with - | O => a - | S n => f (iter f n a) - end. -Infix "^" := iter. - -Lemma iter_alt : forall f n m, (f^(Datatypes.S n)) m = (f^n) (f m). -Proof. -induction n; simpl; auto. -intros; rewrite <- IHn; auto. -Qed. - -Lemma iter_plus : forall f n n' m, (f^(n+n')) m = (f^n) ((f^n') m). -Proof. -induction n; simpl; auto. -intros; rewrite IHn; auto. -Qed. +(** First, some complements about [nat_iter] *) -Lemma iter_plus_bis : forall f n n' m, (f^(n+n')) m = (f^n') ((f^n) m). -Proof. -induction n; simpl; auto. -intros. rewrite <- iter_alt, IHn; auto. -Qed. +Local Notation "f ^ n" := (nat_iter n f). -Global Instance iter_wd (R:relation A) : Proper ((R==>R)==>eq==>R==>R) iter. +Instance nat_iter_wd n {A} (R:relation A) : + Proper ((R==>R)==>R==>R) (nat_iter n). Proof. -intros f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto. +intros f f' Hf. induction n; simpl; red; auto. Qed. -End Iter. -Implicit Arguments iter [A]. -Local Infix "^" := iter. - - Module NZDomainProp (Import NZ:NZDomainSig'). +Include NZBaseProp NZ. (** * Relationship between points thanks to [succ] and [pred]. *) -(** We prove that any points in NZ have a common descendant by [succ] *) - -Definition common_descendant n m := exists k, exists l, (S^k) n == (S^l) m. - -Instance common_descendant_wd : Proper (eq==>eq==>iff) common_descendant. -Proof. -unfold common_descendant. intros n n' Hn m m' Hm. -setoid_rewrite Hn. setoid_rewrite Hm. auto with *. -Qed. - -Instance common_descendant_equiv : Equivalence common_descendant. -Proof. -split; red. -intros x. exists O; exists O. simpl; auto with *. -intros x y (p & q & H); exists q; exists p; auto with *. -intros x y z (p & q & Hpq) (r & s & Hrs). -exists (r+p)%nat. exists (q+s)%nat. -rewrite !iter_plus. rewrite Hpq, <-Hrs, <-iter_plus, <- iter_plus_bis. -auto with *. -Qed. - -Lemma common_descendant_with_0 : forall n, common_descendant n 0. -Proof. -apply bi_induction. -intros n n' Hn. rewrite Hn; auto with *. -reflexivity. -split; intros (p & q & H). -exists p; exists (Datatypes.S q). rewrite <- iter_alt; simpl. - apply succ_wd; auto. -exists (Datatypes.S p); exists q. rewrite iter_alt; auto. -Qed. - -Lemma common_descendant_always : forall n m, common_descendant n m. -Proof. -intros. transitivity 0; [|symmetry]; apply common_descendant_with_0. -Qed. - -(** Thanks to [succ] being injective, we can then deduce that for any two - points, one is an iterated successor of the other. *) +(** For any two points, one is an iterated successor of the other. *) -Lemma itersucc_or_itersucc : forall n m, exists k, n == (S^k) m \/ m == (S^k) n. +Lemma itersucc_or_itersucc n m : exists k, n == (S^k) m \/ m == (S^k) n. Proof. -intros n m. destruct (common_descendant_always n m) as (k & l & H). -revert l H. induction k. -simpl. intros; exists l; left; auto with *. -intros. destruct l. -simpl in *. exists (Datatypes.S k); right; auto with *. -simpl in *. apply pred_wd in H; rewrite !pred_succ in H. eauto. +nzinduct n m. +exists 0%nat. now left. +intros n. split; intros [k [L|R]]. +exists (Datatypes.S k). left. now apply succ_wd. +destruct k as [|k]. +simpl in R. exists 1%nat. left. now apply succ_wd. +rewrite nat_iter_succ_r in R. exists k. now right. +destruct k as [|k]; simpl in L. +exists 1%nat. now right. +apply succ_inj in L. exists k. now left. +exists (Datatypes.S k). right. now rewrite nat_iter_succ_r. Qed. (** Generalized version of [pred_succ] when iterating *) @@ -116,7 +53,7 @@ Proof. induction k. simpl; auto with *. simpl; intros. apply pred_wd in H. rewrite pred_succ in H. apply IHk in H; auto. -rewrite <- iter_alt in H; auto. +rewrite <- nat_iter_succ_r in H; auto. Qed. (** From a given point, all others are iterated successors @@ -307,7 +244,7 @@ End NZOfNat. Module NZOfNatOrd (Import NZ:NZOrdSig'). Include NZOfNat NZ. -Include NZOrderPropFunct NZ. +Include NZBaseProp NZ <+ NZOrderProp NZ. Local Open Scope ofnat. Theorem ofnat_S_gt_0 : @@ -315,8 +252,8 @@ Theorem ofnat_S_gt_0 : Proof. unfold ofnat. intros n; induction n as [| n IH]; simpl in *. -apply lt_0_1. -apply lt_trans with 1. apply lt_0_1. now rewrite <- succ_lt_mono. +apply lt_succ_diag_r. +apply lt_trans with (S 0). apply lt_succ_diag_r. now rewrite <- succ_lt_mono. Qed. Theorem ofnat_S_neq_0 : @@ -375,14 +312,14 @@ Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m. Proof. induction n; intros. apply add_0_l. - rewrite ofnat_succ, add_succ_l. simpl; apply succ_wd; auto. + rewrite ofnat_succ, add_succ_l. simpl. now f_equiv. Qed. Lemma ofnat_add : forall n m, [n+m] == [n]+[m]. Proof. intros. rewrite ofnat_add_l. induction n; simpl. reflexivity. - rewrite ofnat_succ. now apply succ_wd. + rewrite ofnat_succ. now f_equiv. Qed. Lemma ofnat_mul : forall n m, [n*m] == [n]*[m]. @@ -391,14 +328,14 @@ Proof. symmetry. apply mul_0_l. rewrite plus_comm. rewrite ofnat_succ, ofnat_add, mul_succ_l. - now apply add_wd. + now f_equiv. Qed. Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n. Proof. induction m; simpl; intros. rewrite ofnat_zero. apply sub_0_r. - rewrite ofnat_succ, sub_succ_r. now apply pred_wd. + rewrite ofnat_succ, sub_succ_r. now f_equiv. Qed. Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m]. @@ -409,7 +346,7 @@ Proof. intros. destruct n. inversion H. - rewrite iter_alt. + rewrite nat_iter_succ_r. simpl. rewrite ofnat_succ, pred_succ; auto with arith. Qed. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v new file mode 100644 index 00000000..f72023d9 --- /dev/null +++ b/theories/Numbers/NatInt/NZGcd.v @@ -0,0 +1,307 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> t. +End Gcd. + +Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A). + Import A B. + Definition divide n m := exists p, m == p*n. + Local Notation "( n | m )" := (divide n m) (at level 0). + Axiom gcd_divide_l : forall n m, (gcd n m | n). + Axiom gcd_divide_r : forall n m, (gcd n m | m). + Axiom gcd_greatest : forall n m p, (p | n) -> (p | m) -> (p | gcd n m). + Axiom gcd_nonneg : forall n m, 0 <= gcd n m. +End NZGcdSpec. + +Module Type DivideNotation (A:NZOrdAxiomsSig')(B:Gcd A)(C:NZGcdSpec A B). + Import A B C. + Notation "( n | m )" := (divide n m) (at level 0). +End DivideNotation. + +Module Type NZGcd (A : NZOrdAxiomsSig) := Gcd A <+ NZGcdSpec A. +Module Type NZGcd' (A : NZOrdAxiomsSig) := + Gcd A <+ NZGcdSpec A <+ DivideNotation A. + +(** Derived properties of gcd *) + +Module NZGcdProp + (Import A : NZOrdAxiomsSig') + (Import B : NZGcd' A) + (Import C : NZMulOrderProp A). + +(** Results concerning divisibility*) + +Instance divide_wd : Proper (eq==>eq==>iff) divide. +Proof. + unfold divide. intros x x' Hx y y' Hy. + setoid_rewrite Hx. setoid_rewrite Hy. easy. +Qed. + +Lemma divide_1_l : forall n, (1 | n). +Proof. + intros n. exists n. now nzsimpl. +Qed. + +Lemma divide_0_r : forall n, (n | 0). +Proof. + intros n. exists 0. now nzsimpl. +Qed. + +Hint Rewrite divide_1_l divide_0_r : nz. + +Lemma divide_0_l : forall n, (0 | n) -> n==0. +Proof. + intros n (m,Hm). revert Hm. now nzsimpl. +Qed. + +Lemma eq_mul_1_nonneg : forall n m, + 0<=n -> n*m == 1 -> n==1 /\ m==1. +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'. +Qed. + +Lemma eq_mul_1_nonneg' : forall n m, + 0<=m -> n*m == 1 -> n==1 /\ m==1. +Proof. + intros n m Hm H. rewrite mul_comm in H. + now apply and_comm, eq_mul_1_nonneg. +Qed. + +Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1. +Proof. + intros n Hn (m,Hm). symmetry in Hm. + now apply (eq_mul_1_nonneg' m n). +Qed. + +Lemma divide_refl : forall n, (n | n). +Proof. + intros n. exists 1. now nzsimpl. +Qed. + +Lemma divide_trans : forall n m p, (n | m) -> (m | p) -> (n | p). +Proof. + intros n m p (q,Hq) (r,Hr). exists (r*q). + now rewrite Hr, Hq, mul_assoc. +Qed. + +Instance divide_reflexive : Reflexive divide := divide_refl. +Instance divide_transitive : Transitive divide := divide_trans. + +(** Due to sign, no general antisymmetry result *) + +Lemma divide_antisym_nonneg : forall n m, + 0<=n -> 0<=m -> (n | m) -> (m | n) -> 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. +Qed. + +Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m). +Proof. + intros n m p (q,Hq). exists q. now rewrite mul_shuffle3, Hq. +Qed. + +Lemma mul_divide_mono_r : forall n m p, (n | m) -> (n * p | m * p). +Proof. + intros n m p (q,Hq). exists q. now rewrite mul_assoc, Hq. +Qed. + +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. +Qed. + +Lemma mul_divide_cancel_r : forall n m p, p ~= 0 -> + ((n * p | m * p) <-> (n | m)). +Proof. + intros. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l. +Qed. + +Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p). +Proof. + intros n m p (q,Hq) (r,Hr). exists (q+r). + now rewrite mul_add_distr_r, Hq, Hr. +Qed. + +Lemma divide_mul_l : forall n m p, (n | m) -> (n | m * p). +Proof. + intros n m p (q,Hq). exists (q*p). now rewrite mul_shuffle0, Hq. +Qed. + +Lemma divide_mul_r : forall n m p, (n | p) -> (n | m * p). +Proof. + intros n m p. rewrite mul_comm. apply divide_mul_l. +Qed. + +Lemma divide_factor_l : forall n m, (n | n * m). +Proof. + intros. apply divide_mul_l, divide_refl. +Qed. + +Lemma divide_factor_r : forall n m, (n | m * n). +Proof. + intros. apply divide_mul_r, divide_refl. +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. +Qed. + +(** Basic properties of gcd *) + +Lemma gcd_unique : forall n m p, + 0<=p -> (p|n) -> (p|m) -> + (forall q, (q|n) -> (q|m) -> (q|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. +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. +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. +Qed. + +Lemma gcd_unique_alt : forall n m p, 0<=p -> + (forall q, (q|p) <-> (q|n) /\ (q|m)) -> + gcd n m == 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. +Qed. + +Lemma gcd_comm : forall n m, gcd n m == gcd m n. +Proof. + intros. apply gcd_unique_alt; try apply gcd_nonneg. + intros. rewrite and_comm. apply gcd_divide_iff. +Qed. + +Lemma gcd_assoc : forall n m p, gcd n (gcd m p) == gcd (gcd n m) p. +Proof. + intros. apply gcd_unique_alt; try apply gcd_nonneg. + intros. now rewrite !gcd_divide_iff, and_assoc. +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. +Qed. + +Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n. +Proof. + intros. now rewrite gcd_comm, gcd_0_l_nonneg. +Qed. + +Lemma gcd_1_l : forall n, gcd 1 n == 1. +Proof. + intros. apply gcd_unique; trivial using divide_1_l, le_0_1. +Qed. + +Lemma gcd_1_r : forall n, gcd n 1 == 1. +Proof. + intros. now rewrite gcd_comm, gcd_1_l. +Qed. + +Lemma gcd_diag_nonneg : forall n, 0<=n -> gcd n n == n. +Proof. + intros. apply gcd_unique; trivial using divide_refl. +Qed. + +Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0. +Proof. + intros. + generalize (gcd_divide_l n m). rewrite H. apply divide_0_l. +Qed. + +Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0. +Proof. + intros. apply gcd_eq_0_l with n. now rewrite gcd_comm. +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. +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. +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. +Qed. + +End NZGcdProp. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v new file mode 100644 index 00000000..a5aa6d8a --- /dev/null +++ b/theories/Numbers/NatInt/NZLog.v @@ -0,0 +1,889 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t. +End Log2. + +Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A). + Import A B C. + Axiom log2_spec : forall a, 0 2^(log2 a) <= a < 2^(S (log2 a)). + Axiom log2_nonpos : forall a, a<=0 -> log2 a == 0. +End NZLog2Spec. + +Module Type NZLog2 (A : NZOrdAxiomsSig)(B : Pow A) := Log2 A <+ NZLog2Spec A B. + +(** Derived properties of logarithm *) + +Module Type NZLog2Prop + (Import A : NZOrdAxiomsSig') + (Import B : NZPow' A) + (Import C : NZLog2 A B) + (Import D : NZMulOrderProp A) + (Import E : NZPowProp A B D). + +(** log2 is always non-negative *) + +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. +Qed. + +(** A tactic for proving positivity and non-negativity *) + +Ltac order_pos := +((apply add_pos_pos || apply add_nonneg_nonneg || + apply mul_pos_pos || apply mul_nonneg_nonneg || + apply pow_nonneg || apply pow_pos_nonneg || + apply log2_nonneg || apply (le_le_succ_r 0)); + order_pos) (* in case of success of an apply, we recurse *) +|| order'. (* otherwise *) + +(** The spec of log2 indeed determines it *) + +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. +Qed. + +(** Hence log2 is a morphism. *) + +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. +Qed. + +(** An alternate specification *) + +Lemma log2_spec_alt : forall a, 0 exists r, + a == 2^(log2 a) + r /\ 0 <= r < 2^(log2 a). +Proof. + intros a Ha. + 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. +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. +Qed. + +(** log2 is exact on powers of 2 *) + +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. +Qed. + +(** log2 and predecessors of powers of 2 *) + +Lemma log2_pred_pow2 : forall a, 0 log2 (P (2^a)) == P a. +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'. +Qed. + +(** log2 and basic constants *) + +Lemma log2_1 : log2 1 == 0. +Proof. + rewrite <- (pow_0_r 2). now apply log2_pow2. +Qed. + +Lemma log2_2 : log2 2 == 1. +Proof. + rewrite <- (pow_1_r 2). apply log2_pow2; order'. +Qed. + +(** log2 n is strictly positive for 1 0 < log2 a. +Proof. + intros a Ha. + assert (Ha' : 0 < a) by order'. + assert (H := log2_nonneg a). le_elim H; trivial. + generalize (log2_spec a Ha'). rewrite <- H in *. nzsimpl; try order. + intros (_,H'). rewrite two_succ in H'. apply lt_succ_r in H'; order. +Qed. + +(** Said otherwise, log2 is null only below 1 *) + +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. +Qed. + +(** log2 is a monotone function (but not a strict one) *) + +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. +Qed. + +(** No reverse result for <=, consider for instance log2 3 <= log2 2 *) + +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. +Qed. + +(** When left side is a power of 2, we have an equivalence for <= *) + +Lemma log2_le_pow2 : forall a b, 0 (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). +Qed. + +(** When right side is a square, we have an equivalence for < *) + +Lemma log2_lt_pow2 : forall a b, 0 (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. +Qed. + +(** Comparing log2 and identity *) + +Lemma log2_lt_lin : forall a, 0 log2 a < a. +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'. +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. +Qed. + +(** Log2 and multiplication. *) + +(** Due to rounding error, we don't have the usual + [log2 (a*b) = log2 a + log2 b] but we may be off by 1 at most *) + +Lemma log2_mul_below : forall a b, 0 0 + log2 a + log2 b <= log2 (a*b). +Proof. + intros a b Ha Hb. + apply log2_le_pow2; try order_pos. + rewrite pow_add_r by order_pos. + apply mul_le_mono_nonneg; try apply log2_spec; order_pos. +Qed. + +Lemma log2_mul_above : forall a b, 0<=a -> 0<=b -> + log2 (a*b) <= log2 a + log2 b + 1. +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. +Qed. + +(** And we can't find better approximations in general. + - The lower bound is exact for powers of 2. + - Concerning the upper bound, for any c>1, take a=b=2^c-1, + then log2 (a*b) = c+c -1 while (log2 a) = (log2 b) = c-1 +*) + +(** At least, we get back the usual equation when we multiply by 2 (or 2^k) *) + +Lemma log2_mul_pow2 : forall a b, 0 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. +Qed. + +Lemma log2_double : forall a, 0 log2 (2*a) == S (log2 a). +Proof. + intros a Ha. generalize (log2_mul_pow2 a 1 Ha le_0_1). now nzsimpl'. +Qed. + +(** Two numbers with same log2 cannot be far away. *) + +Lemma log2_same : forall a b, 0 0 log2 a == log2 b -> a < 2*b. +Proof. + intros a b Ha Hb H. + apply log2_lt_cancel. rewrite log2_double, H by trivial. + apply lt_succ_diag_r. +Qed. + +(** Log2 and successor : + - the log2 function climbs by at most 1 at a time + - otherwise it stays at the same value + - the +1 steps occur for powers of two +*) + +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. +Qed. + +Lemma log2_succ_or : forall a, + log2 (S a) == S (log2 a) \/ log2 (S a) == log2 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. +Qed. + +Lemma log2_eq_succ_is_pow2 : forall a, + log2 (S a) == S (log2 a) -> exists b, S a == 2^b. +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. +Qed. + +Lemma log2_eq_succ_iff_pow2 : forall a, 0 + (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. +Qed. + +Lemma log2_succ_double : forall a, 0 log2 (2*a+1) == S (log2 a). +Proof. + intros a Ha. + rewrite add_1_r. + 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. +Qed. + +(** Log2 and addition *) + +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. +Qed. + +(** The sum of two log2 is less than twice the log2 of the sum. + The large inequality is obvious thanks to monotonicity. + The strict one requires some more work. This is almost + a convexity inequality for points [2a], [2b] and their middle [a+b] : + ideally, we would have [2*log(a+b) >= log(2a)+log(2b) = 2+log a+log b]. + Here, we cannot do better: consider for instance a=2 b=4, then 1+2<2*2 +*) + +Lemma add_log2_lt : forall a b, 0 0 + log2 a + log2 b < 2 * log2 (a+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. +Qed. + +End NZLog2Prop. + +Module NZLog2UpProp + (Import A : NZDecOrdAxiomsSig') + (Import B : NZPow' A) + (Import C : NZLog2 A B) + (Import D : NZMulOrderProp A) + (Import E : NZPowProp A B D) + (Import F : NZLog2Prop A B C D E). + +(** * [log2_up] : a binary logarithm that rounds up instead of down *) + +(** For once, we define instead of axiomatizing, thanks to log2 *) + +Definition log2_up a := + match compare 1 a with + | Lt => S (log2 (P a)) + | _ => 0 + end. + +Lemma log2_up_eqn0 : forall a, a<=1 -> log2_up a == 0. +Proof. + intros a Ha. unfold log2_up. case compare_spec; try order. +Qed. + +Lemma log2_up_eqn : forall a, 1 log2_up a == S (log2 (P a)). +Proof. + intros a Ha. unfold log2_up. case compare_spec; try order. +Qed. + +Lemma log2_up_spec : forall a, 1 + 2^(P (log2_up a)) < a <= 2^(log2_up a). +Proof. + intros a Ha. + rewrite log2_up_eqn; trivial. + rewrite pred_succ. + rewrite <- (lt_succ_pred 1 a Ha) at 2 3. + rewrite lt_succ_r, le_succ_l. + apply log2_spec. + apply succ_lt_mono. now rewrite (lt_succ_pred 1 a Ha), <- one_succ. +Qed. + +Lemma log2_up_nonpos : forall a, a<=0 -> log2_up a == 0. +Proof. + intros. apply log2_up_eqn0. order'. +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. +Qed. + +(** [log2_up] is always non-negative *) + +Lemma log2_up_nonneg : forall a, 0 <= log2_up a. +Proof. + intros a. unfold log2_up. case compare_spec; try order. + intros. apply le_le_succ_r, log2_nonneg. +Qed. + +(** The spec of [log2_up] indeed determines it *) + +Lemma log2_up_unique : forall a b, 0 2^(P 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. +Qed. + +(** [log2_up] is exact on powers of 2 *) + +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. +Qed. + +(** [log2_up] and successors of powers of 2 *) + +Lemma log2_up_succ_pow2 : forall a, 0<=a -> log2_up (S (2^a)) == S a. +Proof. + intros a Ha. + rewrite log2_up_eqn, pred_succ, log2_pow2; try easy. + rewrite one_succ, <- succ_lt_mono. apply pow_pos_nonneg; order'. +Qed. + +(** Basic constants *) + +Lemma log2_up_1 : log2_up 1 == 0. +Proof. + now apply log2_up_eqn0. +Qed. + +Lemma log2_up_2 : log2_up 2 == 1. +Proof. + rewrite <- (pow_1_r 2). apply log2_up_pow2; order'. +Qed. + +(** Links between log2 and [log2_up] *) + +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. +Qed. + +Lemma le_log2_up_succ_log2 : forall a, log2_up a <= S (log2 a). +Proof. + intros a. unfold log2_up. case compare_spec; intros H; try order_pos. + rewrite <- succ_le_mono. apply log2_le_mono. + rewrite <- (lt_succ_pred 1 a H) at 2. apply le_succ_diag_r. +Qed. + +Lemma log2_log2_up_spec : forall a, 0 + 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. +Qed. + +Lemma log2_log2_up_exact : + forall a, 0 (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. +Qed. + +(** [log2_up] n is strictly positive for 1 0 < log2_up a. +Proof. + intros. rewrite log2_up_eqn; trivial. apply lt_succ_r; order_pos. +Qed. + +(** Said otherwise, [log2_up] is null only below 1 *) + +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. +Qed. + +(** [log2_up] is a monotone function (but not a strict one) *) + +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. +Qed. + +(** No reverse result for <=, consider for instance log2_up 4 <= log2_up 3 *) + +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. +Qed. + +(** When left side is a power of 2, we have an equivalence for < *) + +Lemma log2_up_lt_pow2 : forall a b, 0 (2^b 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. +Qed. + +(** When right side is a square, we have an equivalence for <= *) + +Lemma log2_up_le_pow2 : forall a b, 0 (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'. +Qed. + +(** Comparing [log2_up] and identity *) + +Lemma log2_up_lt_lin : forall a, 0 log2_up a < a. +Proof. + intros a Ha. + 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. +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. +Qed. + +(** [log2_up] and multiplication. *) + +(** Due to rounding error, we don't have the usual + [log2_up (a*b) = log2_up a + log2_up b] but we may be off by 1 at most *) + +Lemma log2_up_mul_above : forall a b, 0<=a -> 0<=b -> + log2_up (a*b) <= log2_up a + log2_up b. +Proof. + intros a b Ha Hb. + 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. +Qed. + +Lemma log2_up_mul_below : forall a b, 0 0 + log2_up a + log2_up b <= S (log2_up (a*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. +Qed. + +(** And we can't find better approximations in general. + - The upper bound is exact for powers of 2. + - Concerning the lower bound, for any c>1, take a=b=2^c+1, + then [log2_up (a*b) = c+c +1] while [(log2_up a) = (log2_up b) = c+1] +*) + +(** At least, we get back the usual equation when we multiply by 2 (or 2^k) *) + +Lemma log2_up_mul_pow2 : forall a b, 0 0<=b -> + log2_up (a*2^b) == b + log2_up a. +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. +Qed. + +Lemma log2_up_double : forall a, 0 log2_up (2*a) == S (log2_up a). +Proof. + intros a Ha. generalize (log2_up_mul_pow2 a 1 Ha le_0_1). now nzsimpl'. +Qed. + +(** Two numbers with same [log2_up] cannot be far away. *) + +Lemma log2_up_same : forall a b, 0 0 log2_up a == log2_up b -> a < 2*b. +Proof. + intros a b Ha Hb H. + apply log2_up_lt_cancel. rewrite log2_up_double, H by trivial. + apply lt_succ_diag_r. +Qed. + +(** [log2_up] and successor : + - the [log2_up] function climbs by at most 1 at a time + - otherwise it stays at the same value + - the +1 steps occur after powers of two +*) + +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. +Qed. + +Lemma log2_up_succ_or : forall a, + log2_up (S a) == S (log2_up a) \/ log2_up (S a) == log2_up 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. +Qed. + +Lemma log2_up_eq_succ_is_pow2 : forall a, + log2_up (S a) == S (log2_up a) -> exists b, a == 2^b. +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. +Qed. + +Lemma log2_up_eq_succ_iff_pow2 : forall a, 0 + (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. +Qed. + +Lemma log2_up_succ_double : forall a, 0 + 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. +Qed. + +(** [log2_up] and addition *) + +Lemma log2_up_add_le : forall a b, a~=1 -> b~=1 -> + log2_up (a+b) <= log2_up a + log2_up b. +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'. +Qed. + +(** The sum of two [log2_up] is less than twice the [log2_up] of the sum. + The large inequality is obvious thanks to monotonicity. + The strict one requires some more work. This is almost + a convexity inequality for points [2a], [2b] and their middle [a+b] : + ideally, we would have [2*log(a+b) >= log(2a)+log(2b) = 2+log a+log b]. + Here, we cannot do better: consider for instance a=3 b=5, then 2+3<2*3 +*) + +Lemma add_log2_up_lt : forall a b, 0 0 + log2_up a + log2_up b < 2 * log2_up (a+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. +Qed. + +End NZLog2UpProp. + diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index b1adcea9..2b5a1cf3 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (p * n < p * m <-> q * n + m < q * m + n). @@ -26,17 +24,16 @@ Qed. Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m). Proof. -nzord_induct p. -intros n m H; false_hyp H lt_irrefl. -intros p H IH n m H1. nzsimpl. -le_elim H. assert (LR : forall n m, n < m -> p * n + n < p * m + m). -intros n1 m1 H2. apply add_lt_mono; [now apply -> IH | assumption]. -split; [apply LR |]. intro H2. apply -> lt_dne; intro H3. -apply <- le_ngt in H3. le_elim H3. -apply lt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 lt_irrefl. -rewrite <- H; now nzsimpl. -intros p H1 _ n m H2. destruct (lt_asymm _ _ H1 H2). +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). @@ -48,19 +45,19 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. nzord_induct p. -intros n m H; false_hyp H lt_irrefl. -intros p H1 _ n m H2. apply lt_succ_l in H2. apply <- nle_gt in H2. -false_hyp H1 H2. -intros p H IH n m H1. apply <- le_succ_l in H. -le_elim H. assert (LR : forall n m, n < m -> p * m < p * n). -intros n1 m1 H2. apply (le_lt_add_lt n1 m1). -now apply lt_le_incl. rewrite <- 2 mul_succ_l. now apply -> IH. -split; [apply LR |]. intro H2. apply -> lt_dne; intro H3. -apply <- le_ngt in H3. le_elim H3. -apply lt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 lt_irrefl. -rewrite (mul_lt_pred p (S p)) by reflexivity. -rewrite H; do 2 rewrite mul_0_l; now do 2 rewrite add_0_l. +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). @@ -72,7 +69,7 @@ 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. +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. @@ -80,7 +77,7 @@ 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. +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. @@ -99,20 +96,13 @@ Qed. Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m). Proof. -intros n m p H; split; intro H1. -destruct (lt_trichotomy p 0) as [H2 | [H2 | H2]]. -apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * m < p * n); [now apply -> mul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 lt_irrefl. -assert (H4 : p * n < p * m); [now apply -> mul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 lt_irrefl. -false_hyp H2 H. -apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * n < p * m) by (now apply -> mul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 lt_irrefl. -assert (H4 : p * m < p * n) by (now apply -> mul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 lt_irrefl. -now rewrite H1. +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. Qed. Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m). @@ -183,17 +173,17 @@ Qed. Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_pos_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_pos_r. Qed. Theorem mul_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r. Qed. Theorem mul_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r. Qed. Theorem mul_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0. @@ -206,9 +196,33 @@ Proof. intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. Qed. +Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m). +Proof. +intros n m Hn. rewrite <- (mul_0_r n) at 1. + symmetry. now apply mul_lt_mono_pos_l. +Qed. + +Theorem mul_pos_cancel_r : forall n m, 0 < m -> (0 < n*m <-> 0 < n). +Proof. +intros n m Hn. rewrite <- (mul_0_l m) at 1. + symmetry. now apply mul_lt_mono_pos_r. +Qed. + +Theorem mul_nonneg_cancel_l : forall n m, 0 < n -> (0 <= n*m <-> 0 <= m). +Proof. +intros n m Hn. rewrite <- (mul_0_r n) at 1. + symmetry. now apply mul_le_mono_pos_l. +Qed. + +Theorem mul_nonneg_cancel_r : forall n m, 0 < m -> (0 <= n*m <-> 0 <= n). +Proof. +intros n m Hn. rewrite <- (mul_0_l m) at 1. + symmetry. now apply mul_le_mono_pos_r. +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. +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. Qed. @@ -229,7 +243,7 @@ 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. +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. @@ -241,16 +255,22 @@ 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]. +intros n m H1 H2. apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. 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]. +intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. false_hyp H1 H2. assumption. Qed. +(** Some alternative names: *) + +Definition mul_eq_0 := eq_mul_0. +Definition mul_eq_0_l := eq_mul_0_l. +Definition mul_eq_0_r := eq_mul_0_r. + Theorem lt_0_mul : forall n m, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). Proof. intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. @@ -283,25 +303,100 @@ 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). -assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonneg. -apply -> le_ngt in F. false_hyp H2 F. +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). -assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonneg. -apply -> lt_nge in F. false_hyp H2 F. +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'. +Qed. + +Lemma add_le_mul : forall a b, 1 1 a+b <= a*b. +Proof. + assert (AUX : forall a b, 0 0 (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. +Qed. + +(** A few results about squares *) + +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. +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. +Qed. + +Lemma add_square_le : forall a b, 0<=a -> 0<=b -> + a*a + b*b <= (a+b)*(a+b). +Proof. + intros a b Ha Hb. + rewrite mul_add_distr_r, !mul_add_distr_l. + rewrite add_assoc. + apply add_le_mono_r. + rewrite <- add_assoc. + rewrite <- (add_0_r (a*a)) at 1. + apply add_le_mono_l. + apply add_nonneg_nonneg; now apply mul_nonneg_nonneg. +Qed. + +Lemma square_add_le : forall a b, 0<=a -> 0<=b -> + (a+b)*(a+b) <= 2*(a*a + b*b). +Proof. + intros a b Ha Hb. + 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. + apply crossmul_le_addsquare; order. Qed. -Theorem mul_2_mono_l : forall n m, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b -> + 2*2*a*b <= (a+b)*(a+b). Proof. -intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m (1 + 1)). -rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l. -apply add_pos_pos; now apply lt_0_1. + intros. + nzsimpl'. + rewrite !mul_add_distr_l, !mul_add_distr_r. + rewrite (add_comm _ (b*b)), add_assoc. + apply add_le_mono_r. + rewrite (add_shuffle0 (a*a)), (mul_comm b a). + apply add_le_mono_r. + rewrite (mul_comm a b) at 1. + now apply crossmul_le_addsquare. Qed. -End NZMulOrderPropSig. +End NZMulOrderProp. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 07805772..8cf5b26f 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* eq==>iff) le. Proof. -intros n n' Hn m m' Hm. rewrite !lt_eq_cases, !Hn, !Hm; auto with *. +intros n n' Hn m m' Hm. now rewrite <- !lt_succ_r, Hn, Hm. Qed. Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H]. Theorem lt_le_incl : forall n m, n < m -> n <= m. Proof. -intros; apply <- lt_eq_cases; now left. +intros. apply lt_eq_cases. now left. Qed. Theorem le_refl : forall n, n <= n. Proof. -intro; apply <- lt_eq_cases; now right. +intro. apply lt_eq_cases. now right. Qed. Theorem lt_succ_diag_r : forall n, n < S n. @@ -99,7 +97,7 @@ 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. +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. @@ -148,7 +146,8 @@ Definition lt_compat := lt_wd. Definition lt_total := lt_trichotomy. Definition le_lteq := lt_eq_cases. -Module OrderElts <: TotalOrder. +Module Private_OrderTac. +Module Elts <: TotalOrder. Definition t := t. Definition eq := eq. Definition lt := lt. @@ -158,9 +157,10 @@ Module OrderElts <: TotalOrder. Definition lt_compat := lt_compat. Definition lt_total := lt_total. Definition le_lteq := le_lteq. -End OrderElts. -Module OrderTac := !MakeOrderTac OrderElts. -Ltac order := OrderTac.order. +End Elts. +Module Tac := !MakeOrderTac Elts. +End Private_OrderTac. +Ltac order := Private_OrderTac.Tac.order. (** Some direct consequences of [order]. *) @@ -208,12 +208,12 @@ Qed. Theorem lt_succ_l : forall n m, S n < m -> n < m. Proof. -intros n m H; apply -> le_succ_l; order. +intros n m H; apply le_succ_l; order. Qed. Theorem le_le_succ_r : forall n m, n <= m -> n <= S m. Proof. -intros n m LE. rewrite <- lt_succ_r in LE. order. +intros n m LE. apply lt_succ_r in LE. order. Qed. Theorem lt_lt_succ_r : forall n m, n < m -> n < S m. @@ -233,19 +233,37 @@ Qed. Theorem lt_0_1 : 0 < 1. Proof. -apply lt_succ_diag_r. +rewrite one_succ. apply lt_succ_diag_r. Qed. Theorem le_0_1 : 0 <= 1. Proof. -apply le_succ_diag_r. +apply lt_le_incl, lt_0_1. Qed. -Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m. +Theorem lt_1_2 : 1 < 2. +Proof. +rewrite two_succ. apply lt_succ_diag_r. +Qed. + +Theorem lt_0_2 : 0 < 2. +Proof. +transitivity 1. apply lt_0_1. apply lt_1_2. +Qed. + +Theorem le_0_2 : 0 <= 2. Proof. -intros n m H1 H2. apply <- le_succ_l in H1. order. +apply lt_le_incl, lt_0_2. Qed. +(** The order tactic enriched with some knowledge of 0,1,2 *) + +Ltac order' := generalize lt_0_1 lt_1_2; order. + +Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m. +Proof. +intros n m H1 H2. rewrite <- le_succ_l, <- one_succ in H1. order. +Qed. (** More Trichotomy, decidability and double negation elimination. *) @@ -347,7 +365,7 @@ 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]. +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. @@ -359,6 +377,13 @@ intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). assumption. apply le_refl. Qed. +Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n. +Proof. + intros z n H. + destruct (lt_exists_pred _ _ H) as (n' & EQ & LE). + rewrite EQ. now rewrite pred_succ. +Qed. + (** Stronger variant of induction with assumptions n >= 0 (n < 0) in the induction step *) @@ -390,14 +415,14 @@ 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; +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. Proof. -intros m H1 H2. apply -> le_ngt in H1. false_hyp H2 H1. +intros m H1 H2. apply le_ngt in H1. false_hyp H2 H1. Qed. Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n. @@ -449,28 +474,28 @@ 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]. +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. +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. +apply le_succ_l in H3. now apply H1. rewrite <- H3 in *; now apply LS'. Qed. Lemma lbase : A' (S z). Proof. -intros m H1 H2. apply -> le_succ_l in H2. -apply -> le_ngt in H1. false_hyp H2 H1. +intros m H1 H2. apply le_succ_l in H2. +apply le_ngt in H1. false_hyp H2 H1. Qed. Lemma A'A_left : (forall n, A' n) -> forall n, n <= z -> A n. Proof. -intros H1 n H2. apply H1 with (n := n); [assumption | now apply eq_le_incl]. +intros H1 n H2. apply (H1 n); [assumption | now apply eq_le_incl]. Qed. Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n. @@ -527,8 +552,8 @@ Theorem order_induction' : forall n, A n. Proof. intros Az AS AP n; apply order_induction; try assumption. -intros m H1 H2. apply AP in H2; [| now apply <- le_succ_l]. -apply -> (A_wd (P (S m)) m); [assumption | apply pred_succ]. +intros m H1 H2. apply AP in H2; [|now apply le_succ_l]. +now rewrite pred_succ in H2. Qed. End Center. @@ -555,11 +580,11 @@ Theorem lt_ind : forall (n : t), forall m, n < m -> A m. Proof. intros n H1 H2 m H3. -apply right_induction with (S n); [assumption | | now apply <- le_succ_l]. -intros; apply H2; try assumption. now apply -> le_succ_l. +apply right_induction with (S n); [assumption | | now apply le_succ_l]. +intros; apply H2; try assumption. now apply le_succ_l. Qed. -(** Elimintation principle for <= *) +(** Elimination principle for <= *) Theorem le_ind : forall (n : t), A n -> @@ -582,8 +607,8 @@ Section WF. Variable z : t. -Let Rlt (n m : t) := z <= n /\ n < m. -Let Rgt (n m : t) := m < n /\ n <= z. +Let Rlt (n m : t) := z <= n < m. +Let Rgt (n m : t) := m < n <= z. Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt. Proof. @@ -595,25 +620,13 @@ Proof. intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2. Qed. -Instance Acc_lt_wd : Proper (eq==>iff) (Acc Rlt). -Proof. -intros x1 x2 H; split; intro H1; destruct H1 as [H2]; -constructor; intros; apply H2; now (rewrite H || rewrite <- H). -Qed. - -Instance Acc_gt_wd : Proper (eq==>iff) (Acc Rgt). -Proof. -intros x1 x2 H; split; intro H1; destruct H1 as [H2]; -constructor; intros; apply H2; now (rewrite H || rewrite <- H). -Qed. - Theorem lt_wf : well_founded Rlt. Proof. unfold well_founded. apply strong_right_induction' with (z := z). -apply Acc_lt_wd. +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. +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. @@ -621,24 +634,20 @@ Theorem gt_wf : well_founded Rgt. Proof. unfold well_founded. apply strong_left_induction' with (z := z). -apply Acc_gt_wd. +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. +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. +apply H2. assumption. now apply le_succ_l. Qed. End WF. -End NZOrderPropSig. - -Module NZOrderPropFunct (NZ : NZOrdSig) := - NZBasePropSig NZ <+ NZOrderPropSig NZ. +End NZOrderProp. (** If we have moreover a [compare] function, we can build an [OrderedType] structure. *) -Module NZOrderedTypeFunct (NZ : NZDecOrdSig') - <: DecidableTypeFull <: OrderedTypeFull := - NZ <+ NZOrderPropFunct <+ Compare2EqBool <+ HasEqBool2Dec. - +Module NZOrderedType (NZ : NZDecOrdSig') + <: DecidableTypeFull <: OrderedTypeFull + := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v new file mode 100644 index 00000000..29109ccb --- /dev/null +++ b/theories/Numbers/NatInt/NZParity.v @@ -0,0 +1,263 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool. + Definition Even n := exists m, n == 2*m. + Definition Odd n := exists m, n == 2*m+1. + Axiom even_spec : forall n, even n = true <-> Even n. + Axiom odd_spec : forall n, odd n = true <-> Odd n. +End NZParity. + +Module Type NZParityProp + (Import A : NZOrdAxiomsSig') + (Import B : NZParity A) + (Import C : NZMulOrderProp A). + +(** Morphisms *) + +Instance Even_wd : Proper (eq==>iff) Even. +Proof. unfold Even. solve_proper. Qed. + +Instance Odd_wd : Proper (eq==>iff) Odd. +Proof. unfold Odd. solve_proper. Qed. + +Instance even_wd : Proper (eq==>Logic.eq) even. +Proof. + intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now f_equiv. +Qed. + +Instance odd_wd : Proper (eq==>Logic.eq) odd. +Proof. + intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now f_equiv. +Qed. + +(** Evenness and oddity are dual notions *) + +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 2*n < 2*m+1. +Proof. + intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono. +Qed. + +Lemma double_above : forall n m, n 2*n+1 < 2*m. +Proof. + intros. nzsimpl'. + rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r. + apply add_le_mono; now apply le_succ_l. +Qed. + +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. +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. +Qed. + +Lemma negb_odd : forall n, negb (odd n) = even n. +Proof. + intros. + generalize (Even_or_Odd n) (Even_Odd_False n). + rewrite <- even_spec, <- odd_spec. + destruct (odd n), (even n); simpl; intuition. +Qed. + +Lemma negb_even : forall n, negb (even n) = odd n. +Proof. + intros. rewrite <- negb_odd. apply negb_involutive. +Qed. + +(** Constants *) + +Lemma even_0 : even 0 = true. +Proof. + rewrite even_spec. exists 0. now nzsimpl. +Qed. + +Lemma odd_0 : odd 0 = false. +Proof. + now rewrite <- negb_even, even_0. +Qed. + +Lemma odd_1 : odd 1 = true. +Proof. + rewrite odd_spec. exists 0. now nzsimpl'. +Qed. + +Lemma even_1 : even 1 = false. +Proof. + now rewrite <- negb_odd, odd_1. +Qed. + +Lemma even_2 : even 2 = true. +Proof. + rewrite even_spec. exists 1. now nzsimpl'. +Qed. + +Lemma odd_2 : odd 2 = false. +Proof. + now rewrite <- negb_even, even_2. +Qed. + +(** Parity and successor *) + +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. +Qed. + +Lemma odd_succ : forall n, odd (S n) = even n. +Proof. + intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec. + apply Odd_succ. +Qed. + +Lemma even_succ : forall n, even (S n) = odd n. +Proof. + intros. now rewrite <- negb_odd, odd_succ, negb_even. +Qed. + +Lemma Even_succ : forall n, Even (S n) <-> Odd n. +Proof. + intros. now rewrite <- even_spec, even_succ, odd_spec. +Qed. + +(** Parity and successor of successor *) + +Lemma Even_succ_succ : forall n, Even (S (S n)) <-> Even n. +Proof. + intros. now rewrite Even_succ, Odd_succ. +Qed. + +Lemma Odd_succ_succ : forall n, Odd (S (S n)) <-> Odd n. +Proof. + intros. now rewrite Odd_succ, Even_succ. +Qed. + +Lemma even_succ_succ : forall n, even (S (S n)) = even n. +Proof. + intros. now rewrite even_succ, odd_succ. +Qed. + +Lemma odd_succ_succ : forall n, odd (S (S n)) = odd n. +Proof. + intros. now rewrite odd_succ, even_succ. +Qed. + +(** Parity and addition *) + +Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m). +Proof. + intros. + 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. +Qed. + +Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). +Proof. + intros. rewrite <- !negb_even. rewrite even_add. + now destruct (even n), (even m). +Qed. + +(** Parity and multiplication *) + +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. +Qed. + +Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. +Proof. + intros. rewrite <- !negb_even. rewrite even_mul. + now destruct (even n), (even m). +Qed. + +(** A particular case : adding by an even number *) + +Lemma even_add_even : forall n m, Even m -> even (n+m) = even n. +Proof. + intros n m Hm. apply even_spec in Hm. + rewrite even_add, Hm. now destruct (even n). +Qed. + +Lemma odd_add_even : forall n m, Even m -> odd (n+m) = odd n. +Proof. + intros n m Hm. apply even_spec in Hm. + rewrite odd_add, <- (negb_even m), Hm. now destruct (odd n). +Qed. + +Lemma even_add_mul_even : forall n m p, Even m -> even (n+m*p) = even n. +Proof. + intros n m p Hm. apply even_spec in Hm. + apply even_add_even. apply even_spec. now rewrite even_mul, Hm. +Qed. + +Lemma odd_add_mul_even : forall n m p, Even m -> odd (n+m*p) = odd n. +Proof. + intros n m p Hm. apply even_spec in Hm. + apply odd_add_even. apply even_spec. now rewrite even_mul, Hm. +Qed. + +Lemma even_add_mul_2 : forall n m, even (n+2*m) = even n. +Proof. + intros. apply even_add_mul_even. apply even_spec, even_2. +Qed. + +Lemma odd_add_mul_2 : forall n m, odd (n+2*m) = odd n. +Proof. + intros. apply odd_add_mul_even. apply even_spec, even_2. +Qed. + +End NZParityProp. \ No newline at end of file diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v new file mode 100644 index 00000000..58704735 --- /dev/null +++ b/theories/Numbers/NatInt/NZPow.v @@ -0,0 +1,411 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> t. +End Pow. + +Module Type PowNotation (A : Typ)(Import B : Pow A). + Infix "^" := pow. +End PowNotation. + +Module Type Pow' (A : Typ) := Pow A <+ PowNotation A. + +Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A). + Declare Instance pow_wd : Proper (eq==>eq==>eq) pow. + Axiom pow_0_r : forall a, a^0 == 1. + Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. + Axiom pow_neg_r : forall a b, b<0 -> a^b == 0. +End NZPowSpec. + +(** The above [pow_neg_r] specification is useless (and trivially + provable) for N. Having it here allows to already derive + some slightly more general statements. *) + +Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A. +Module Type NZPow' (A : NZOrdAxiomsSig) := Pow' A <+ NZPowSpec A. + +(** Derived properties of power *) + +Module Type NZPowProp + (Import A : NZOrdAxiomsSig') + (Import B : NZPow' A) + (Import C : NZMulOrderProp A). + +Hint Rewrite pow_0_r pow_succ_r : nz. + +(** Power and basic constants *) + +Lemma pow_0_l : forall a, 0 0^a == 0. +Proof. + intros a Ha. + destruct (lt_exists_pred _ _ Ha) as (a' & EQ & Ha'). + rewrite EQ. now nzsimpl. +Qed. + +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. +Qed. + +Lemma pow_1_r : forall a, a^1 == a. +Proof. + intros. now nzsimpl'. +Qed. + +Lemma pow_1_l : forall a, 0<=a -> 1^a == 1. +Proof. + apply le_ind; intros. solve_proper. + now nzsimpl. + now nzsimpl. +Qed. + +Hint Rewrite pow_1_r pow_1_l : nz. + +Lemma pow_2_r : forall a, a^2 == a*a. +Proof. + intros. rewrite two_succ. nzsimpl; order'. +Qed. + +Hint Rewrite pow_2_r : nz. + +(** Power and nullity *) + +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. +Qed. + +Lemma pow_nonzero : forall a b, a~=0 -> 0<=b -> a^b ~= 0. +Proof. + intros a b Ha Hb. contradict Ha. now apply pow_eq_0 with b. +Qed. + +Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0 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. +Qed. + +Lemma pow_mul_l : forall a b c, + (a*b)^c == a^c * 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. +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. +Qed. + +(** Positivity *) + +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. +Qed. + +Lemma pow_pos_nonneg : forall a b, 0 0<=b -> 0 0<=a 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. +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. +Qed. + +Lemma pow_gt_1 : forall a b, 1 (0 1 0<=c -> b 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. +Qed. + +(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *) + +Lemma pow_le_mono_r : forall a b c, 0 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. +Qed. + +Lemma pow_le_mono : forall a b c d, 0 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. +Qed. + +Lemma pow_lt_mono : forall a b c d, 0 0 + a^b < c^d. +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. +Qed. + +(** Injectivity *) + +Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0 + a^c == b^c -> a == b. +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. +Qed. + +Lemma pow_inj_r : forall a b c, 1 0<=b -> 0<=c -> + a^b == a^c -> b == 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. +Qed. + +(** Monotonicity results, both ways *) + +Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0 + (a a^c < b^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. +Qed. + +Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0 + (a<=b <-> a^c <= b^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. +Qed. + +Lemma pow_lt_mono_r_iff : forall a b c, 1 0<=c -> + (b a^b < a^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. +Qed. + +Lemma pow_le_mono_r_iff : forall a b c, 1 0<=c -> + (b<=c <-> a^b <= a^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. +Qed. + +(** For any a>1, the a^x function is above the identity function *) + +Lemma pow_gt_lin_r : forall a b, 1 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. +Qed. + +(** Someday, we should say something about the full Newton formula. + In the meantime, we can at least provide some inequalities about + (a+b)^c. +*) + +Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0 + 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. +Qed. + +(** This upper bound can also be seen as a convexity proof for x^c : + image of (a+b)/2 is below the middle of the images of a and b +*) + +Lemma pow_add_upper : forall a b c, 0<=a -> 0<=b -> 0 + (a+b)^c <= 2^(pred c) * (a^c + b^c). +Proof. + assert (aux : forall a b c, 0<=a<=b -> 0 + (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'. +Qed. + +End NZPowProp. diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v index 7279325d..13c26233 100644 --- a/theories/Numbers/NatInt/NZProperties.v +++ b/theories/Numbers/NatInt/NZProperties.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* t. +End Sqrt. + +Module Type SqrtNotation (A : Typ)(Import B : Sqrt A). + Notation "√ x" := (sqrt x) (at level 6). +End SqrtNotation. + +Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A. + +Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A). + Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a). + Axiom sqrt_neg : forall a, a<0 -> √a == 0. +End NZSqrtSpec. + +Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A. +Module Type NZSqrt' (A : NZOrdAxiomsSig) := Sqrt' A <+ NZSqrtSpec A. + +(** Derived properties of power *) + +Module Type NZSqrtProp + (Import A : NZOrdAxiomsSig') + (Import B : NZSqrt' A) + (Import C : NZMulOrderProp A). + +Local Notation "a ²" := (a*a) (at level 5, no associativity, format "a ²"). + +(** First, sqrt is non-negative *) + +Lemma sqrt_spec_nonneg : forall b, + b² < (S b)² -> 0 <= b. +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. +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. +Qed. + +(** The spec of sqrt indeed determines it *) + +Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b. +Proof. + intros a b (LEb,LTb). + assert (Ha : 0<=a) by (transitivity b²; trivial using square_nonneg). + assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order). + 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. +Qed. + +(** Hence sqrt is a morphism *) + +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. +Qed. + +(** An alternate specification *) + +Lemma sqrt_spec_alt : forall a, 0<=a -> exists r, + a == (√a)² + r /\ 0 <= r <= 2*√a. +Proof. + intros a Ha. + 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. +Qed. + +Lemma sqrt_unique' : forall a b c, 0<=c<=2*b -> + a == b² + c -> √a == b. +Proof. + intros a b c (Hc,H) EQ. + 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'. +Qed. + +(** Sqrt is exact on squares *) + +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. +Qed. + +(** Sqrt and predecessors of squares *) + +Lemma sqrt_pred_square : forall a, 0 √(P a²) == P a. +Proof. + intros a Ha. + 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. +Qed. + +(** Sqrt is a monotone function (but not a strict one) *) + +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. +Qed. + +(** No reverse result for <=, consider for instance √2 <= √1 *) + +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. +Qed. + +(** When left side is a square, we have an equivalence for <= *) + +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. +Qed. + +(** When right side is a square, we have an equivalence for < *) + +Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a √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. +Qed. + +(** Sqrt and basic constants *) + +Lemma sqrt_0 : √0 == 0. +Proof. + rewrite <- (mul_0_l 0) at 1. now apply sqrt_square. +Qed. + +Lemma sqrt_1 : √1 == 1. +Proof. + rewrite <- (mul_1_l 1) at 1. apply sqrt_square. order'. +Qed. + +Lemma sqrt_2 : √2 == 1. +Proof. + 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. +Qed. + +Lemma sqrt_lt_lin : forall a, 1 √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. +Qed. + +(** Sqrt and multiplication. *) + +(** Due to rounding error, we don't have the usual √(a*b) = √a*√b + but only lower and upper bounds. *) + +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. +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. +Qed. + +(** And we can't find better approximations in general. + - The lower bound is exact for squares + - Concerning the upper bound, for any c>0, take a=b=c²-1, + then √(a*b) = c² -1 while S √a = S √b = c +*) + +(** Sqrt and successor : + - the sqrt function climbs by at most 1 at a time + - otherwise it stays at the same value + - the +1 steps occur for squares +*) + +Lemma sqrt_succ_le : forall a, 0<=a -> √(S a) <= S (√a). +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. +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. +Qed. + +Lemma sqrt_eq_succ_iff_square : forall a, 0<=a -> + (√(S a) == S (√a) <-> exists b, 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 + of square roots. *) + +Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> √a + √b <= √(2*(a+b)). +Proof. + intros a b Ha Hb. + 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. +Qed. + +End NZSqrtProp. + +Module Type NZSqrtUpProp + (Import A : NZDecOrdAxiomsSig') + (Import B : NZSqrt' A) + (Import C : NZMulOrderProp A) + (Import D : NZSqrtProp A B C). + +(** * [sqrt_up] : a square root that rounds up instead of down *) + +Local Notation "a ²" := (a*a) (at level 5, no associativity, format "a ²"). + +(** For once, we define instead of axiomatizing, thanks to sqrt *) + +Definition sqrt_up a := + match compare 0 a with + | Lt => S √(P a) + | _ => 0 + end. + +Local Notation "√° a" := (sqrt_up a) (at level 6, no associativity). + +Lemma sqrt_up_eqn0 : forall a, a<=0 -> √°a == 0. +Proof. + intros a Ha. unfold sqrt_up. case compare_spec; try order. +Qed. + +Lemma sqrt_up_eqn : forall a, 0 √°a == S √(P a). +Proof. + intros a Ha. unfold sqrt_up. case compare_spec; try order. +Qed. + +Lemma sqrt_up_spec : forall a, 0 (P √°a)² < a <= (√°a)². +Proof. + intros a Ha. + rewrite sqrt_up_eqn, pred_succ; trivial. + assert (Ha' := lt_succ_pred 0 a Ha). + rewrite <- Ha' at 3 4. + rewrite le_succ_l, lt_succ_r. + apply sqrt_spec. + now rewrite <- lt_succ_r, Ha'. +Qed. + +(** First, [sqrt_up] is non-negative *) + +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. +Qed. + +(** [sqrt_up] is a morphism *) + +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. +Qed. + +(** The spec of [sqrt_up] indeed determines it *) + +Lemma sqrt_up_unique : forall a b, 0 (P b)² < a <= b² -> √°a == b. +Proof. + intros a b Hb (LEb,LTb). + assert (Ha : 0 √°(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. +Qed. + +(** [sqrt_up] and successors of squares *) + +Lemma sqrt_up_succ_square : forall a, 0<=a -> √°(S a²) == S a. +Proof. + intros a Ha. + rewrite sqrt_up_eqn by (now apply lt_succ_r, mul_nonneg_nonneg). + now rewrite pred_succ, sqrt_square. +Qed. + +(** Basic constants *) + +Lemma sqrt_up_0 : √°0 == 0. +Proof. + rewrite <- (mul_0_l 0) at 1. now apply sqrt_up_square. +Qed. + +Lemma sqrt_up_1 : √°1 == 1. +Proof. + rewrite <- (mul_1_l 1) at 1. apply sqrt_up_square. order'. +Qed. + +Lemma sqrt_up_2 : √°2 == 2. +Proof. + rewrite sqrt_up_eqn by order'. + now rewrite two_succ, pred_succ, sqrt_1. +Qed. + +(** Links between sqrt and [sqrt_up] *) + +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. +Qed. + +Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a). +Proof. + intros a. unfold sqrt_up. + case compare_spec; intros H; try apply le_le_succ_r, sqrt_nonneg. + rewrite <- succ_le_mono. apply sqrt_le_mono. + rewrite <- (lt_succ_pred 0 a H) at 2. apply le_succ_diag_r. +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. +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. +Qed. + +(** [sqrt_up] is a monotone function (but not a strict one) *) + +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. +Qed. + +(** No reverse result for <=, consider for instance √°3 <= √°2 *) + +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. +Qed. + +(** When left side is a square, we have an equivalence for < *) + +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. +Qed. + +(** When right side is a square, we have an equivalence for <= *) + +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. +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. +Qed. + +Lemma sqrt_up_lt_lin : forall a, 2 √°a < a. +Proof. + intros a Ha. + rewrite sqrt_up_eqn by order'. + assert (Ha' := lt_succ_pred 2 a Ha). + rewrite <- Ha' at 2. rewrite <- succ_lt_mono. + apply sqrt_lt_lin. rewrite succ_lt_mono. now rewrite Ha', <- two_succ. +Qed. + +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. +Qed. + +(** [sqrt_up] and multiplication. *) + +(** Due to rounding error, we don't have the usual [√(a*b) = √a*√b] + but only lower and upper bounds. *) + +Lemma sqrt_up_mul_above : forall a b, 0<=a -> 0<=b -> √°(a*b) <= √°a * √°b. +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. +Qed. + +Lemma sqrt_up_mul_below : forall a b, 0 0 (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. +Qed. + +(** And we can't find better approximations in general. + - The upper bound is exact for squares + - Concerning the lower bound, for any c>0, take [a=b=c²+1], + then [√°(a*b) = c²+1] while [P √°a = P √°b = c] +*) + +(** [sqrt_up] and successor : + - the [sqrt_up] function climbs by at most 1 at a time + - otherwise it stays at the same value + - the +1 steps occur after squares +*) + +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. +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. +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. +Qed. + +(** [sqrt_up] and addition *) + +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. +Qed. + +(** Convexity-like inequality for [sqrt_up]: [sqrt_up] of middle is above middle + of square roots. We cannot say more, for instance take a=b=2, then + 2+2 <= S 3 *) + +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'. +Qed. + +End NZSqrtUpProp. -- cgit v1.2.3 From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- .gitignore | 5 +- CHANGES | 166 +- COMPATIBILITY | 47 +- INSTALL | 2 +- INSTALL.macosx | 20 - Makefile | 36 +- Makefile.build | 33 +- Makefile.common | 23 +- TODO | 53 + checker/check.ml | 2 +- checker/check_stat.ml | 2 +- checker/check_stat.mli | 2 +- checker/checker.ml | 2 +- checker/closure.ml | 2 +- checker/closure.mli | 2 +- checker/indtypes.ml | 2 +- checker/indtypes.mli | 2 +- checker/inductive.ml | 2 +- checker/inductive.mli | 2 +- checker/mod_checking.mli | 2 +- checker/modops.ml | 2 +- checker/modops.mli | 2 +- checker/reduction.ml | 2 +- checker/reduction.mli | 2 +- checker/safe_typing.ml | 2 +- checker/safe_typing.mli | 2 +- checker/subtyping.ml | 2 +- checker/subtyping.mli | 2 +- checker/term.ml | 2 +- checker/type_errors.ml | 2 +- checker/type_errors.mli | 2 +- checker/typeops.ml | 2 +- checker/typeops.mli | 2 +- checker/validate.ml | 2 +- config/Makefile.template | 154 -- config/coq_config.mli | 2 +- configure | 478 ++--- dev/db_printers.ml | 2 +- dev/header | 2 +- dev/macosify_accel.sh | 3 + dev/top_printers.ml | 4 +- doc/refman/RefMan-sch.tex | 418 ----- doc/stdlib/index-list.html.template | 6 + ide/command_windows.ml | 2 +- ide/command_windows.mli | 2 +- ide/config_lexer.mll | 2 +- ide/coq.ml | 2 +- ide/coq.mli | 2 +- ide/coq_commands.ml | 2 +- ide/coq_lex.mll | 2 +- ide/coqide.ml | 13 +- ide/coqide.mli | 2 +- ide/coqide_main.ml4 | 2 +- ide/gtk_parsing.ml | 2 +- ide/ide_mac_stubs.c | 10 +- ide/ideproof.ml | 40 +- ide/ideutils.ml | 2 +- ide/ideutils.mli | 2 +- ide/mac_default_accel_map | 726 ++++---- ide/minilib.ml | 55 +- ide/preferences.ml | 4 +- ide/preferences.mli | 2 +- ide/project_file.ml4 | 2 +- ide/tags.ml | 2 +- ide/tags.mli | 2 +- ide/typed_notebook.ml | 2 +- ide/undo.ml | 2 +- ide/undo_lablgtk_ge212.mli | 2 +- ide/undo_lablgtk_ge26.mli | 2 +- ide/undo_lablgtk_lt26.mli | 2 +- ide/utf8_convert.mll | 2 +- interp/constrextern.ml | 58 +- interp/constrextern.mli | 4 +- interp/constrintern.ml | 31 +- interp/constrintern.mli | 2 +- interp/coqlib.ml | 2 +- interp/coqlib.mli | 2 +- interp/dumpglob.ml | 2 +- interp/dumpglob.mli | 2 +- interp/genarg.ml | 2 +- interp/genarg.mli | 2 +- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- interp/modintern.ml | 2 +- interp/modintern.mli | 2 +- interp/notation.ml | 35 +- interp/notation.mli | 2 +- interp/ppextend.ml | 2 +- interp/ppextend.mli | 2 +- interp/reserve.ml | 2 +- interp/reserve.mli | 2 +- interp/smartlocate.ml | 2 +- interp/smartlocate.mli | 2 +- interp/syntax_def.ml | 66 +- interp/syntax_def.mli | 12 +- interp/topconstr.ml | 2 +- interp/topconstr.mli | 2 +- kernel/cbytecodes.ml | 2 +- kernel/cbytecodes.mli | 4 +- kernel/cbytegen.ml | 2 +- kernel/cemitcodes.ml | 2 +- kernel/closure.ml | 2 +- kernel/closure.mli | 2 +- kernel/conv_oracle.ml | 2 +- kernel/conv_oracle.mli | 2 +- kernel/cooking.ml | 8 +- kernel/cooking.mli | 5 +- kernel/csymtable.ml | 2 +- kernel/csymtable.mli | 4 +- kernel/declarations.ml | 2 +- kernel/declarations.mli | 2 +- kernel/entries.ml | 2 +- kernel/entries.mli | 2 +- kernel/environ.ml | 2 +- kernel/environ.mli | 2 +- kernel/esubst.ml | 2 +- kernel/esubst.mli | 2 +- kernel/indtypes.ml | 2 +- kernel/indtypes.mli | 2 +- kernel/inductive.ml | 2 +- kernel/inductive.mli | 2 +- kernel/mod_subst.ml | 2 +- kernel/mod_subst.mli | 2 +- kernel/mod_typing.ml | 2 +- kernel/mod_typing.mli | 2 +- kernel/modops.ml | 2 +- kernel/modops.mli | 2 +- kernel/names.ml | 2 +- kernel/names.mli | 2 +- kernel/pre_env.ml | 2 +- kernel/pre_env.mli | 2 +- kernel/reduction.ml | 2 +- kernel/reduction.mli | 2 +- kernel/retroknowledge.ml | 2 +- kernel/retroknowledge.mli | 2 +- kernel/safe_typing.ml | 2 +- kernel/safe_typing.mli | 2 +- kernel/sign.ml | 2 +- kernel/sign.mli | 2 +- kernel/subtyping.ml | 2 +- kernel/subtyping.mli | 2 +- kernel/term.ml | 3 +- kernel/term.mli | 3 +- kernel/term_typing.ml | 5 +- kernel/term_typing.mli | 2 +- kernel/type_errors.ml | 2 +- kernel/type_errors.mli | 2 +- kernel/typeops.ml | 2 +- kernel/typeops.mli | 2 +- kernel/univ.ml | 2 +- kernel/univ.mli | 2 +- kernel/vconv.mli | 2 +- kernel/vm.ml | 2 +- lib/bigint.ml | 355 ++-- lib/bigint.mli | 11 +- lib/compat.ml4 | 2 +- lib/dnet.ml | 2 +- lib/dnet.mli | 2 +- lib/dyn.ml | 2 +- lib/dyn.mli | 2 +- lib/envars.ml | 10 +- lib/envars.mli | 2 +- lib/explore.ml | 2 +- lib/explore.mli | 2 +- lib/flags.ml | 17 +- lib/flags.mli | 7 +- lib/gmap.ml | 2 +- lib/gmap.mli | 2 +- lib/gmapl.ml | 2 +- lib/gmapl.mli | 2 +- lib/hashcons.ml | 2 +- lib/hashcons.mli | 2 +- lib/hashtbl_alt.ml | 2 +- lib/hashtbl_alt.mli | 2 +- lib/heap.ml | 2 +- lib/heap.mli | 2 +- lib/option.ml | 2 +- lib/option.mli | 2 +- lib/pp.ml4 | 13 +- lib/pp.mli | 6 +- lib/pp_control.ml | 2 +- lib/pp_control.mli | 2 +- lib/profile.ml | 2 +- lib/profile.mli | 2 +- lib/rtree.ml | 2 +- lib/rtree.mli | 2 +- lib/system.ml | 2 +- lib/system.mli | 2 +- lib/tries.ml | 2 +- lib/unionfind.ml | 2 +- lib/unionfind.mli | 2 +- lib/util.mli | 2 +- lib/xml_lexer.mll | 6 + library/assumptions.ml | 2 +- library/assumptions.mli | 2 +- library/decl_kinds.ml | 2 +- library/decl_kinds.mli | 2 +- library/declare.ml | 2 +- library/declare.mli | 2 +- library/declaremods.ml | 2 +- library/declaremods.mli | 2 +- library/decls.ml | 2 +- library/decls.mli | 2 +- library/dischargedhypsmap.ml | 2 +- library/dischargedhypsmap.mli | 2 +- library/global.ml | 2 +- library/global.mli | 2 +- library/goptions.ml | 2 +- library/goptions.mli | 2 +- library/goptionstyp.mli | 2 +- library/heads.ml | 2 +- library/heads.mli | 2 +- library/impargs.ml | 2 +- library/impargs.mli | 2 +- library/lib.ml | 2 +- library/lib.mli | 2 +- library/libnames.ml | 2 +- library/libnames.mli | 2 +- library/libobject.ml | 2 +- library/libobject.mli | 2 +- library/library.ml | 2 +- library/library.mli | 2 +- library/nameops.ml | 2 +- library/nameops.mli | 2 +- library/nametab.ml | 2 +- library/nametab.mli | 2 +- library/states.ml | 2 +- library/states.mli | 2 +- library/summary.ml | 2 +- library/summary.mli | 2 +- parsing/argextend.ml4 | 2 +- parsing/egrammar.ml | 2 +- parsing/egrammar.mli | 2 +- parsing/extend.ml | 2 +- parsing/extend.mli | 2 +- parsing/extrawit.ml | 2 +- parsing/extrawit.mli | 2 +- parsing/g_constr.ml4 | 2 +- parsing/g_ltac.ml4 | 3 +- parsing/g_prim.ml4 | 2 +- parsing/g_proofs.ml4 | 2 +- parsing/g_tactic.ml4 | 58 +- parsing/g_vernac.ml4 | 19 +- parsing/g_xml.ml4 | 2 +- parsing/lexer.ml4 | 2 +- parsing/lexer.mli | 2 +- parsing/pcoq.ml4 | 2 +- parsing/pcoq.mli | 2 +- parsing/ppconstr.ml | 30 +- parsing/ppconstr.mli | 9 +- parsing/pptactic.ml | 31 +- parsing/pptactic.mli | 2 +- parsing/ppvernac.ml | 22 +- parsing/ppvernac.mli | 4 +- parsing/prettyp.ml | 14 +- parsing/prettyp.mli | 2 +- parsing/printer.ml | 119 +- parsing/printer.mli | 6 +- parsing/printmod.ml | 6 +- parsing/printmod.mli | 2 +- parsing/q_constr.ml4 | 2 +- parsing/q_coqast.ml4 | 24 +- parsing/q_util.ml4 | 2 +- parsing/q_util.mli | 2 +- parsing/tacextend.ml4 | 8 +- parsing/tactic_printer.ml | 2 +- parsing/tactic_printer.mli | 2 +- parsing/tok.ml | 2 +- parsing/tok.mli | 2 +- parsing/vernacextend.ml4 | 13 +- plugins/cc/ccalgo.ml | 2 +- plugins/cc/ccalgo.mli | 2 +- plugins/cc/ccproof.ml | 2 +- plugins/cc/ccproof.mli | 2 +- plugins/cc/cctac.ml | 8 +- plugins/cc/cctac.mli | 2 +- plugins/cc/g_congruence.ml4 | 2 +- plugins/decl_mode/decl_expr.mli | 2 +- plugins/decl_mode/decl_interp.ml | 2 +- plugins/decl_mode/decl_interp.mli | 2 +- plugins/decl_mode/decl_mode.ml | 2 +- plugins/decl_mode/decl_mode.mli | 2 +- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/decl_mode/decl_proof_instr.mli | 2 +- plugins/decl_mode/g_decl_mode.ml4 | 2 +- plugins/decl_mode/ppdecl_proof.ml | 2 +- plugins/extraction/ExtrOcamlBasic.v | 2 +- plugins/extraction/ExtrOcamlBigIntConv.v | 2 +- plugins/extraction/ExtrOcamlIntConv.v | 2 +- plugins/extraction/ExtrOcamlNatBigInt.v | 2 +- plugins/extraction/ExtrOcamlNatInt.v | 2 +- plugins/extraction/ExtrOcamlString.v | 2 +- plugins/extraction/ExtrOcamlZBigInt.v | 8 +- plugins/extraction/ExtrOcamlZInt.v | 4 +- plugins/extraction/big.ml | 2 +- plugins/extraction/common.ml | 4 +- plugins/extraction/common.mli | 2 +- plugins/extraction/extract_env.ml | 6 +- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/extraction.ml | 2 +- plugins/extraction/extraction.mli | 2 +- plugins/extraction/g_extraction.ml4 | 2 +- plugins/extraction/haskell.ml | 2 +- plugins/extraction/haskell.mli | 2 +- plugins/extraction/miniml.mli | 2 +- plugins/extraction/mlutil.ml | 2 +- plugins/extraction/mlutil.mli | 2 +- plugins/extraction/modutil.ml | 2 +- plugins/extraction/modutil.mli | 2 +- plugins/extraction/ocaml.ml | 2 +- plugins/extraction/ocaml.mli | 2 +- plugins/extraction/scheme.ml | 2 +- plugins/extraction/scheme.mli | 2 +- plugins/extraction/table.ml | 3 +- plugins/extraction/table.mli | 2 +- plugins/field/LegacyField.v | 2 +- plugins/field/LegacyField_Compl.v | 2 +- plugins/field/LegacyField_Tactic.v | 22 +- plugins/field/LegacyField_Theory.v | 182 +- plugins/field/field.ml4 | 2 +- plugins/firstorder/formula.ml | 2 +- plugins/firstorder/formula.mli | 2 +- plugins/firstorder/g_ground.ml4 | 2 +- plugins/firstorder/ground.ml | 2 +- plugins/firstorder/ground.mli | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/firstorder/instances.mli | 2 +- plugins/firstorder/rules.ml | 2 +- plugins/firstorder/rules.mli | 2 +- plugins/firstorder/sequent.ml | 2 +- plugins/firstorder/sequent.mli | 2 +- plugins/firstorder/unify.ml | 2 +- plugins/firstorder/unify.mli | 2 +- plugins/fourier/Fourier.v | 2 +- plugins/fourier/Fourier_util.v | 34 +- plugins/fourier/fourier.ml | 2 +- plugins/fourier/fourierR.ml | 2 +- plugins/fourier/g_fourier.ml4 | 2 +- plugins/funind/Recdef.v | 2 +- plugins/funind/functional_principles_types.ml | 6 - plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/micromega/CheckerMaker.v | 2 +- plugins/micromega/Env.v | 153 +- plugins/micromega/EnvRing.v | 1257 +++++-------- plugins/micromega/MExtraction.v | 4 +- plugins/micromega/OrderedRing.v | 2 +- plugins/micromega/Psatz.v | 8 +- plugins/micromega/QMicromega.v | 10 +- plugins/micromega/RMicromega.v | 30 +- plugins/micromega/Refl.v | 2 +- plugins/micromega/RingMicromega.v | 50 +- plugins/micromega/Tauto.v | 2 +- plugins/micromega/VarMap.v | 2 +- plugins/micromega/ZCoeff.v | 16 +- plugins/micromega/ZMicromega.v | 216 ++- plugins/micromega/certificate.ml | 2 +- plugins/micromega/coq_micromega.ml | 23 +- plugins/micromega/csdpcert.ml | 2 +- plugins/micromega/g_micromega.ml4 | 2 +- plugins/micromega/mutils.ml | 2 +- plugins/micromega/persistent_cache.ml | 32 +- plugins/micromega/polynomial.ml | 2 +- plugins/micromega/sos.mli | 2 +- plugins/micromega/sos_types.ml | 2 +- plugins/nsatz/Nsatz.v | 40 +- plugins/nsatz/ideal.ml | 2 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/nsatz/polynom.ml | 2 +- plugins/nsatz/polynom.mli | 2 +- plugins/omega/Omega.v | 8 +- plugins/omega/OmegaLemmas.v | 266 ++- plugins/omega/OmegaPlugin.v | 2 +- plugins/omega/PreOmega.v | 353 ++-- plugins/omega/coq_omega.ml | 59 +- plugins/omega/g_omega.ml4 | 2 +- plugins/omega/omega.ml | 2 +- plugins/quote/Quote.v | 4 +- plugins/quote/g_quote.ml4 | 2 +- plugins/quote/quote.ml | 2 +- plugins/ring/LegacyArithRing.v | 8 +- plugins/ring/LegacyNArithRing.v | 25 +- plugins/ring/LegacyRing.v | 6 +- plugins/ring/LegacyRing_theory.v | 42 +- plugins/ring/LegacyZArithRing.v | 8 +- plugins/ring/Ring_abstract.v | 90 +- plugins/ring/Ring_normalize.v | 142 +- plugins/ring/Setoid_ring.v | 2 +- plugins/ring/Setoid_ring_normalize.v | 122 +- plugins/ring/Setoid_ring_theory.v | 4 +- plugins/ring/g_ring.ml4 | 2 +- plugins/ring/ring.ml | 8 +- plugins/romega/ReflOmegaCore.v | 505 +++-- plugins/rtauto/Bintree.v | 16 +- plugins/rtauto/Rtauto.v | 2 +- plugins/rtauto/g_rtauto.ml4 | 2 +- plugins/rtauto/proof_search.ml | 2 +- plugins/rtauto/proof_search.mli | 2 +- plugins/rtauto/refl_tauto.ml | 4 +- plugins/rtauto/refl_tauto.mli | 2 +- plugins/setoid_ring/ArithRing.v | 10 +- plugins/setoid_ring/BinList.v | 77 +- plugins/setoid_ring/Cring.v | 27 +- plugins/setoid_ring/Field.v | 2 +- plugins/setoid_ring/Field_tac.v | 6 +- plugins/setoid_ring/Field_theory.v | 415 ++--- plugins/setoid_ring/InitialRing.v | 108 +- plugins/setoid_ring/Integral_domain.v | 5 +- plugins/setoid_ring/NArithRing.v | 2 +- plugins/setoid_ring/Ncring.v | 35 +- plugins/setoid_ring/Ncring_initial.v | 56 +- plugins/setoid_ring/Ncring_polynom.v | 111 +- plugins/setoid_ring/Ncring_tac.v | 10 +- plugins/setoid_ring/RealField.v | 64 +- plugins/setoid_ring/Ring.v | 4 +- plugins/setoid_ring/Ring_base.v | 2 +- plugins/setoid_ring/Ring_polynom.v | 1310 +++++-------- plugins/setoid_ring/Ring_tac.v | 7 +- plugins/setoid_ring/Ring_theory.v | 293 ++- plugins/setoid_ring/Rings_Z.v | 2 +- plugins/setoid_ring/ZArithRing.v | 6 +- plugins/setoid_ring/newring.ml4 | 2 +- plugins/subtac/eterm.mli | 2 +- plugins/subtac/g_subtac.ml4 | 2 +- plugins/subtac/subtac.ml | 2 +- plugins/subtac/subtac_cases.ml | 2 +- plugins/subtac/subtac_cases.mli | 2 +- plugins/subtac/subtac_classes.ml | 2 +- plugins/subtac/subtac_classes.mli | 2 +- plugins/subtac/subtac_coercion.ml | 2 +- plugins/subtac/subtac_command.ml | 9 +- plugins/subtac/subtac_pretyping.ml | 2 +- plugins/subtac/subtac_pretyping_F.ml | 2 +- plugins/syntax/nat_syntax.ml | 6 +- plugins/syntax/numbers_syntax.ml | 96 +- plugins/syntax/r_syntax.ml | 2 +- plugins/syntax/z_syntax.ml | 2 +- plugins/xml/dumptree.ml4 | 2 +- pretyping/arguments_renaming.ml | 2 +- pretyping/arguments_renaming.mli | 2 +- pretyping/cases.ml | 2 +- pretyping/cases.mli | 2 +- pretyping/cbv.ml | 2 +- pretyping/cbv.mli | 2 +- pretyping/classops.ml | 2 +- pretyping/classops.mli | 2 +- pretyping/coercion.ml | 2 +- pretyping/coercion.mli | 2 +- pretyping/detyping.ml | 2 +- pretyping/detyping.mli | 2 +- pretyping/evarconv.ml | 36 +- pretyping/evarconv.mli | 2 +- pretyping/evarutil.ml | 85 +- pretyping/evarutil.mli | 24 +- pretyping/evd.ml | 2 +- pretyping/evd.mli | 2 +- pretyping/glob_term.ml | 2 +- pretyping/glob_term.mli | 2 +- pretyping/indrec.ml | 2 +- pretyping/indrec.mli | 2 +- pretyping/inductiveops.ml | 2 +- pretyping/inductiveops.mli | 2 +- pretyping/matching.ml | 2 +- pretyping/matching.mli | 2 +- pretyping/namegen.ml | 2 +- pretyping/namegen.mli | 2 +- pretyping/pattern.ml | 2 +- pretyping/pattern.mli | 2 +- pretyping/pretype_errors.ml | 2 +- pretyping/pretype_errors.mli | 2 +- pretyping/pretyping.ml | 16 +- pretyping/pretyping.mli | 2 +- pretyping/recordops.ml | 2 +- pretyping/recordops.mli | 2 +- pretyping/reductionops.ml | 2 +- pretyping/reductionops.mli | 2 +- pretyping/retyping.ml | 2 +- pretyping/retyping.mli | 2 +- pretyping/tacred.ml | 2 +- pretyping/tacred.mli | 2 +- pretyping/term_dnet.ml | 2 +- pretyping/term_dnet.mli | 2 +- pretyping/termops.ml | 2 +- pretyping/termops.mli | 2 +- pretyping/typeclasses.ml | 2 +- pretyping/typeclasses.mli | 2 +- pretyping/typeclasses_errors.ml | 2 +- pretyping/typeclasses_errors.mli | 2 +- pretyping/typing.ml | 2 +- pretyping/typing.mli | 2 +- pretyping/unification.ml | 26 +- pretyping/unification.mli | 2 +- pretyping/vnorm.ml | 2 +- pretyping/vnorm.mli | 2 +- proofs/clenv.ml | 2 +- proofs/clenv.mli | 2 +- proofs/clenvtac.ml | 6 +- proofs/clenvtac.mli | 2 +- proofs/evar_refiner.ml | 2 +- proofs/evar_refiner.mli | 2 +- proofs/goal.ml | 2 +- proofs/goal.mli | 2 +- proofs/logic.ml | 2 +- proofs/logic.mli | 2 +- proofs/pfedit.ml | 5 +- proofs/pfedit.mli | 2 +- proofs/proof.ml | 18 +- proofs/proof.mli | 11 +- proofs/proof_global.ml | 2 +- proofs/proof_global.mli | 2 +- proofs/proof_type.ml | 2 +- proofs/proof_type.mli | 2 +- proofs/proofview.ml | 7 +- proofs/proofview.mli | 20 +- proofs/redexpr.ml | 2 +- proofs/redexpr.mli | 2 +- proofs/refiner.ml | 2 +- proofs/refiner.mli | 2 +- proofs/tacexpr.ml | 14 +- proofs/tacmach.ml | 2 +- proofs/tacmach.mli | 2 +- proofs/tactic_debug.ml | 2 +- proofs/tactic_debug.mli | 2 +- scripts/coqc.ml | 2 +- scripts/coqmktop.ml | 41 +- states/MakeInitial.v | 2 +- tactics/auto.ml | 26 +- tactics/auto.mli | 2 +- tactics/autorewrite.ml | 2 +- tactics/autorewrite.mli | 2 +- tactics/btermdn.ml | 2 +- tactics/btermdn.mli | 2 +- tactics/class_tactics.ml4 | 2 +- tactics/contradiction.ml | 2 +- tactics/contradiction.mli | 2 +- tactics/eauto.ml4 | 2 +- tactics/eauto.mli | 2 +- tactics/elim.ml | 2 +- tactics/elim.mli | 2 +- tactics/elimschemes.ml | 2 +- tactics/elimschemes.mli | 2 +- tactics/eqdecide.ml4 | 2 +- tactics/eqschemes.ml | 2 +- tactics/eqschemes.mli | 2 +- tactics/equality.ml | 2 +- tactics/equality.mli | 2 +- tactics/evar_tactics.ml | 2 +- tactics/evar_tactics.mli | 2 +- tactics/extraargs.ml4 | 2 +- tactics/extraargs.mli | 2 +- tactics/extratactics.ml4 | 8 +- tactics/extratactics.mli | 2 +- tactics/hiddentac.ml | 25 +- tactics/hiddentac.mli | 21 +- tactics/hipattern.ml4 | 2 +- tactics/hipattern.mli | 2 +- tactics/inv.ml | 2 +- tactics/inv.mli | 2 +- tactics/leminv.ml | 2 +- tactics/nbtermdn.ml | 2 +- tactics/nbtermdn.mli | 2 +- tactics/refine.ml | 2 +- tactics/refine.mli | 2 +- tactics/rewrite.ml4 | 247 ++- tactics/tacinterp.ml | 65 +- tactics/tacinterp.mli | 3 +- tactics/tactic_option.ml | 2 +- tactics/tactic_option.mli | 2 +- tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 2 +- tactics/tactics.ml | 21 +- tactics/tactics.mli | 6 +- tactics/tauto.ml4 | 2 +- tactics/termdn.ml | 2 +- tactics/termdn.mli | 2 +- test-suite/bench/lists-100.v | 2 +- test-suite/bench/lists_100.v | 2 +- test-suite/bugs/closed/shouldsucceed/1414.v | 4 +- test-suite/bugs/closed/shouldsucceed/1784.v | 2 +- test-suite/bugs/closed/shouldsucceed/1844.v | 2 +- test-suite/bugs/closed/shouldsucceed/1935.v | 2 +- test-suite/bugs/closed/shouldsucceed/2127.v | 4 +- test-suite/bugs/closed/shouldsucceed/2817.v | 9 + test-suite/bugs/closed/shouldsucceed/2836.v | 39 + test-suite/complexity/ring2.v | 7 +- test-suite/failure/Tauto.v | 2 +- test-suite/failure/Uminus.v | 4 +- test-suite/failure/clash_cons.v | 2 +- test-suite/failure/fixpoint1.v | 2 +- test-suite/failure/guard.v | 2 +- test-suite/failure/illtype1.v | 2 +- test-suite/failure/pattern.v | 2 +- test-suite/failure/positivity.v | 2 +- test-suite/failure/redef.v | 2 +- test-suite/failure/search.v | 2 +- test-suite/failure/subtyping2.v | 20 +- test-suite/failure/universes-buraliforti-redef.v | 20 +- test-suite/failure/universes-buraliforti.v | 20 +- test-suite/ideal-features/Apply.v | 2 +- test-suite/ideal-features/eapply_evar.v | 2 +- test-suite/micromega/example.v | 10 +- test-suite/micromega/square.v | 18 +- test-suite/misc/berardi_test.v | 14 +- test-suite/modules/PO.v | 4 +- test-suite/modules/Przyklad.v | 14 +- test-suite/output/Notations.out | 5 + test-suite/output/Notations.v | 9 + test-suite/output/ZSyntax.out | 14 +- test-suite/success/Check.v | 2 +- test-suite/success/Field.v | 2 +- test-suite/success/Funind.v | 22 +- test-suite/success/Hints.v | 26 +- test-suite/success/LegacyField.v | 2 +- test-suite/success/MatchFail.v | 4 +- test-suite/success/Mod_type.v | 12 + test-suite/success/Notations.v | 5 + test-suite/success/OmegaPre.v | 16 +- test-suite/success/ProgramWf.v | 6 +- test-suite/success/ROmegaPre.v | 16 +- test-suite/success/RecTutorial.v | 10 +- test-suite/success/Reg.v | 8 +- test-suite/success/Scopes.v | 2 +- test-suite/success/Tauto.v | 2 +- test-suite/success/TestRefine.v | 2 +- test-suite/success/Try.v | 2 +- test-suite/success/apply.v | 6 +- test-suite/success/change.v | 6 +- test-suite/success/decl_mode.v | 10 +- test-suite/success/dependentind.v | 2 +- test-suite/success/eauto.v | 2 +- test-suite/success/eqdecide.v | 2 +- test-suite/success/extraction.v | 2 +- test-suite/success/fix.v | 8 +- test-suite/success/inds_type_sec.v | 2 +- test-suite/success/induct.v | 2 +- test-suite/success/ltac.v | 8 +- test-suite/success/mutual_ind.v | 2 +- test-suite/success/proof_using.v | 6 + test-suite/success/remember.v | 2 +- test-suite/success/searchabout.v | 2 +- test-suite/success/setoid_test.v | 20 +- test-suite/success/specialize.v | 28 +- test-suite/success/unfold.v | 2 +- test-suite/success/unicode_utf8.v | 2 +- test-suite/success/univers.v | 4 +- test-suite/typeclasses/NewSetoid.v | 2 +- theories/Arith/Arith.v | 2 +- theories/Arith/Arith_base.v | 2 +- theories/Arith/Between.v | 8 +- theories/Arith/Bool_nat.v | 4 +- theories/Arith/Compare.v | 8 +- theories/Arith/Compare_dec.v | 10 +- theories/Arith/Div2.v | 18 +- theories/Arith/EqNat.v | 18 +- theories/Arith/Euclid.v | 20 +- theories/Arith/Even.v | 6 +- theories/Arith/Factorial.v | 8 +- theories/Arith/Gt.v | 16 +- theories/Arith/Le.v | 8 +- theories/Arith/Lt.v | 12 +- theories/Arith/Max.v | 2 +- theories/Arith/Min.v | 4 +- theories/Arith/Minus.v | 32 +- theories/Arith/Mult.v | 24 +- theories/Arith/Peano_dec.v | 6 +- theories/Arith/Plus.v | 32 +- theories/Arith/Wf_nat.v | 22 +- theories/Bool/Bool.v | 8 +- theories/Bool/BoolEq.v | 6 +- theories/Bool/Bvector.v | 4 +- theories/Bool/DecBool.v | 2 +- theories/Bool/IfProp.v | 2 +- theories/Bool/Sumbool.v | 2 +- theories/Bool/Zerob.v | 4 +- theories/Classes/EquivDec.v | 4 +- theories/Classes/Equivalence.v | 6 +- theories/Classes/Init.v | 2 +- theories/Classes/Morphisms.v | 4 +- theories/Classes/Morphisms_Prop.v | 2 +- theories/Classes/Morphisms_Relations.v | 2 +- theories/Classes/RelationClasses.v | 4 +- theories/Classes/SetoidClass.v | 2 +- theories/Classes/SetoidDec.v | 4 +- theories/Classes/SetoidTactics.v | 4 +- theories/FSets/FMapAVL.v | 20 +- theories/FSets/FMapFullAVL.v | 4 +- theories/FSets/FMapPositive.v | 2 +- theories/FSets/FSetBridge.v | 148 +- theories/FSets/FSetEqProperties.v | 8 +- theories/FSets/FSetFacts.v | 6 +- theories/FSets/FSetProperties.v | 2 +- theories/Init/Datatypes.v | 24 +- theories/Init/Logic.v | 24 +- theories/Init/Logic_Type.v | 12 +- theories/Init/Notations.v | 2 +- theories/Init/Peano.v | 26 +- theories/Init/Prelude.v | 2 +- theories/Init/Specif.v | 28 +- theories/Init/Tactics.v | 12 +- theories/Init/Wf.v | 4 +- theories/Lists/List.v | 48 +- theories/Lists/ListSet.v | 78 +- theories/Lists/ListTactics.v | 4 +- theories/Lists/SetoidList.v | 90 +- theories/Lists/SetoidPermutation.v | 125 ++ theories/Lists/StreamMemo.v | 29 +- theories/Lists/Streams.v | 14 +- theories/Lists/vo.itarget | 1 + theories/Logic/Berardi.v | 14 +- theories/Logic/ChoiceFacts.v | 6 +- theories/Logic/Classical.v | 2 +- theories/Logic/ClassicalChoice.v | 2 +- theories/Logic/ClassicalDescription.v | 4 +- theories/Logic/ClassicalEpsilon.v | 2 +- theories/Logic/ClassicalFacts.v | 38 +- theories/Logic/ClassicalUniqueChoice.v | 2 +- theories/Logic/Classical_Pred_Set.v | 2 +- theories/Logic/Classical_Pred_Type.v | 10 +- theories/Logic/Classical_Prop.v | 10 +- theories/Logic/Classical_Type.v | 2 +- theories/Logic/ConstructiveEpsilon.v | 6 +- theories/Logic/Decidable.v | 2 +- theories/Logic/Description.v | 2 +- theories/Logic/Diaconescu.v | 16 +- theories/Logic/Epsilon.v | 2 +- theories/Logic/Eqdep.v | 2 +- theories/Logic/EqdepFacts.v | 14 +- theories/Logic/Eqdep_dec.v | 32 +- theories/Logic/ExtensionalityFacts.v | 2 +- theories/Logic/FunctionalExtensionality.v | 2 +- theories/Logic/Hurkens.v | 6 +- theories/Logic/IndefiniteDescription.v | 2 +- theories/Logic/JMeq.v | 2 +- theories/Logic/ProofIrrelevance.v | 2 +- theories/Logic/ProofIrrelevanceFacts.v | 4 +- theories/Logic/RelationalChoice.v | 2 +- theories/Logic/SetIsType.v | 2 +- theories/MSets/MSetEqProperties.v | 8 +- theories/MSets/MSetInterface.v | 2 +- theories/MSets/MSetList.v | 6 +- theories/MSets/MSetPositive.v | 4 +- theories/MSets/MSetProperties.v | 2 +- theories/MSets/MSetRBT.v | 104 +- theories/MSets/MSetWeakList.v | 6 +- theories/NArith/BinNat.v | 220 +-- theories/NArith/BinNatDef.v | 94 +- theories/NArith/NArith.v | 2 +- theories/NArith/Ndec.v | 443 ++--- theories/NArith/Ndigits.v | 207 +-- theories/NArith/Ndist.v | 104 +- theories/NArith/Ndiv_def.v | 14 +- theories/NArith/Ngcd_def.v | 2 +- theories/NArith/Nnat.v | 56 +- theories/NArith/Nsqrt_def.v | 12 +- theories/Numbers/BigNumPrelude.v | 163 +- theories/Numbers/BinNums.v | 2 +- theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 46 +- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 14 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 50 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 115 +- .../Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 30 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 272 +-- theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 80 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 186 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 88 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 393 ++-- theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v | 26 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 4 +- theories/Numbers/Cyclic/Int31/Cyclic31.v | 609 +++--- theories/Numbers/Cyclic/Int31/Int31.v | 18 +- theories/Numbers/Cyclic/Int31/Ring31.v | 4 +- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 191 +- theories/Numbers/Integer/Abstract/ZAdd.v | 2 +- theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZAxioms.v | 2 +- theories/Numbers/Integer/Abstract/ZBase.v | 2 +- theories/Numbers/Integer/Abstract/ZBits.v | 4 +- theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +- theories/Numbers/Integer/Abstract/ZDivFloor.v | 4 +- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +- theories/Numbers/Integer/Abstract/ZGcd.v | 2 +- theories/Numbers/Integer/Abstract/ZLcm.v | 2 +- theories/Numbers/Integer/Abstract/ZLt.v | 2 +- theories/Numbers/Integer/Abstract/ZMaxMin.v | 2 +- theories/Numbers/Integer/Abstract/ZMul.v | 2 +- theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZParity.v | 2 +- theories/Numbers/Integer/Abstract/ZPow.v | 13 +- theories/Numbers/Integer/Abstract/ZProperties.v | 2 +- theories/Numbers/Integer/Abstract/ZSgnAbs.v | 2 +- theories/Numbers/Integer/BigZ/BigZ.v | 10 +- theories/Numbers/Integer/BigZ/ZMake.v | 454 ++--- theories/Numbers/Integer/Binary/ZBinary.v | 4 +- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 4 +- theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 +- theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 6 +- theories/Numbers/NaryFunctions.v | 2 +- theories/Numbers/NatInt/NZAdd.v | 2 +- theories/Numbers/NatInt/NZAddOrder.v | 2 +- theories/Numbers/NatInt/NZAxioms.v | 4 +- theories/Numbers/NatInt/NZBase.v | 2 +- theories/Numbers/NatInt/NZBits.v | 2 +- theories/Numbers/NatInt/NZDiv.v | 2 +- theories/Numbers/NatInt/NZDomain.v | 2 +- theories/Numbers/NatInt/NZGcd.v | 2 +- theories/Numbers/NatInt/NZLog.v | 2 +- theories/Numbers/NatInt/NZMul.v | 2 +- theories/Numbers/NatInt/NZMulOrder.v | 6 +- theories/Numbers/NatInt/NZOrder.v | 2 +- theories/Numbers/NatInt/NZParity.v | 2 +- theories/Numbers/NatInt/NZPow.v | 2 +- theories/Numbers/NatInt/NZProperties.v | 2 +- theories/Numbers/NatInt/NZSqrt.v | 2 +- theories/Numbers/Natural/Abstract/NAdd.v | 2 +- theories/Numbers/Natural/Abstract/NAddOrder.v | 2 +- theories/Numbers/Natural/Abstract/NAxioms.v | 2 +- theories/Numbers/Natural/Abstract/NBase.v | 2 +- theories/Numbers/Natural/Abstract/NBits.v | 4 +- theories/Numbers/Natural/Abstract/NDefOps.v | 4 +- theories/Numbers/Natural/Abstract/NDiv.v | 2 +- theories/Numbers/Natural/Abstract/NGcd.v | 2 +- theories/Numbers/Natural/Abstract/NIso.v | 2 +- theories/Numbers/Natural/Abstract/NLcm.v | 2 +- theories/Numbers/Natural/Abstract/NLog.v | 2 +- theories/Numbers/Natural/Abstract/NMaxMin.v | 2 +- theories/Numbers/Natural/Abstract/NMulOrder.v | 2 +- theories/Numbers/Natural/Abstract/NOrder.v | 2 +- theories/Numbers/Natural/Abstract/NParity.v | 2 +- theories/Numbers/Natural/Abstract/NPow.v | 2 +- theories/Numbers/Natural/Abstract/NProperties.v | 2 +- theories/Numbers/Natural/Abstract/NSqrt.v | 2 +- theories/Numbers/Natural/Abstract/NStrongRec.v | 2 +- theories/Numbers/Natural/Abstract/NSub.v | 2 +- theories/Numbers/Natural/BigN/BigN.v | 4 +- theories/Numbers/Natural/BigN/NMake.v | 364 ++-- theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +- theories/Numbers/Natural/BigN/Nbasic.v | 120 +- theories/Numbers/Natural/Binary/NBinary.v | 6 +- theories/Numbers/Natural/Peano/NPeano.v | 2 +- theories/Numbers/Natural/SpecViaZ/NSig.v | 2 +- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 10 +- theories/Numbers/NumPrelude.v | 2 +- theories/Numbers/Rational/BigQ/BigQ.v | 10 +- theories/Numbers/Rational/BigQ/QMake.v | 485 +++-- theories/Numbers/Rational/SpecViaQ/QSig.v | 2 +- theories/PArith/BinPos.v | 364 ++-- theories/PArith/BinPosDef.v | 5 +- theories/PArith/PArith.v | 2 +- theories/PArith/POrderedType.v | 2 +- theories/PArith/Pnat.v | 81 +- theories/Program/Basics.v | 4 +- theories/Program/Combinators.v | 2 +- theories/Program/Equality.v | 12 +- theories/Program/Program.v | 2 +- theories/Program/Subset.v | 6 +- theories/Program/Syntax.v | 2 +- theories/Program/Tactics.v | 4 +- theories/Program/Utils.v | 2 +- theories/Program/Wf.v | 6 +- theories/QArith/QArith.v | 2 +- theories/QArith/QArith_base.v | 255 ++- theories/QArith/QOrderedType.v | 2 +- theories/QArith/Qabs.v | 26 +- theories/QArith/Qcanon.v | 22 +- theories/QArith/Qfield.v | 6 +- theories/QArith/Qminmax.v | 2 +- theories/QArith/Qpower.v | 88 +- theories/QArith/Qreals.v | 62 +- theories/QArith/Qreduction.v | 166 +- theories/QArith/Qring.v | 2 +- theories/QArith/Qround.v | 26 +- theories/Reals/Alembert.v | 254 +-- theories/Reals/AltSeries.v | 122 +- theories/Reals/ArithProp.v | 50 +- theories/Reals/Binomial.v | 68 +- theories/Reals/Cauchy_prod.v | 28 +- theories/Reals/Cos_plus.v | 194 +- theories/Reals/Cos_rel.v | 92 +- theories/Reals/DiscrR.v | 10 +- theories/Reals/Exp_prop.v | 230 ++- theories/Reals/Integration.v | 2 +- theories/Reals/LegacyRfield.v | 6 +- theories/Reals/MVT.v | 102 +- theories/Reals/Machin.v | 168 ++ theories/Reals/NewtonInt.v | 158 +- theories/Reals/PSeries_reg.v | 62 +- theories/Reals/PartSum.v | 142 +- theories/Reals/RIneq.v | 266 +-- theories/Reals/RList.v | 232 +-- theories/Reals/ROrderedType.v | 2 +- theories/Reals/R_Ifp.v | 80 +- theories/Reals/R_sqr.v | 36 +- theories/Reals/R_sqrt.v | 56 +- theories/Reals/Ranalysis.v | 775 +------- theories/Reals/Ranalysis1.v | 362 ++-- theories/Reals/Ranalysis2.v | 92 +- theories/Reals/Ranalysis3.v | 162 +- theories/Reals/Ranalysis4.v | 106 +- theories/Reals/Ranalysis5.v | 1348 ++++++++++++++ theories/Reals/Ranalysis_reg.v | 800 ++++++++ theories/Reals/Ratan.v | 1602 ++++++++++++++++ theories/Reals/Raxioms.v | 8 +- theories/Reals/Rbase.v | 2 +- theories/Reals/Rbasic_fun.v | 102 +- theories/Reals/Rcomplete.v | 50 +- theories/Reals/Rdefinitions.v | 4 +- theories/Reals/Rderiv.v | 114 +- theories/Reals/Reals.v | 2 +- theories/Reals/Rfunctions.v | 119 +- theories/Reals/Rgeom.v | 32 +- theories/Reals/RiemannInt.v | 898 ++++----- theories/Reals/RiemannInt_SF.v | 954 +++++----- theories/Reals/Rlimit.v | 106 +- theories/Reals/Rlogic.v | 10 +- theories/Reals/Rminmax.v | 2 +- theories/Reals/Rpow_def.v | 2 +- theories/Reals/Rpower.v | 168 +- theories/Reals/Rprod.v | 20 +- theories/Reals/Rseries.v | 44 +- theories/Reals/Rsigma.v | 34 +- theories/Reals/Rsqrt_def.v | 216 +-- theories/Reals/Rtopology.v | 694 +++---- theories/Reals/Rtrigo.v | 1796 +----------------- theories/Reals/Rtrigo1.v | 1933 ++++++++++++++++++++ theories/Reals/Rtrigo_alt.v | 163 +- theories/Reals/Rtrigo_calc.v | 112 +- theories/Reals/Rtrigo_def.v | 108 +- theories/Reals/Rtrigo_fun.v | 30 +- theories/Reals/Rtrigo_reg.v | 308 +--- theories/Reals/SeqProp.v | 270 +-- theories/Reals/SeqSeries.v | 98 +- theories/Reals/SplitAbsolu.v | 4 +- theories/Reals/SplitRmult.v | 2 +- theories/Reals/Sqrt_reg.v | 150 +- theories/Reals/vo.itarget | 5 + theories/Relations/Operators_Properties.v | 8 +- theories/Relations/Relation_Definitions.v | 2 +- theories/Relations/Relation_Operators.v | 8 +- theories/Relations/Relations.v | 8 +- theories/Setoids/Setoid.v | 2 +- theories/Sets/Classical_sets.v | 18 +- theories/Sets/Constructive_sets.v | 18 +- theories/Sets/Cpo.v | 2 +- theories/Sets/Ensembles.v | 2 +- theories/Sets/Finite_sets.v | 6 +- theories/Sets/Finite_sets_facts.v | 20 +- theories/Sets/Image.v | 12 +- theories/Sets/Infinite_sets.v | 14 +- theories/Sets/Integers.v | 24 +- theories/Sets/Multiset.v | 18 +- theories/Sets/Partial_Order.v | 20 +- theories/Sets/Permut.v | 2 +- theories/Sets/Powerset.v | 28 +- theories/Sets/Powerset_Classical_facts.v | 42 +- theories/Sets/Powerset_facts.v | 36 +- theories/Sets/Relations_1.v | 2 +- theories/Sets/Relations_1_facts.v | 20 +- theories/Sets/Relations_2.v | 2 +- theories/Sets/Relations_2_facts.v | 14 +- theories/Sets/Relations_3.v | 2 +- theories/Sets/Relations_3_facts.v | 28 +- theories/Sets/Uniset.v | 30 +- theories/Sorting/Heap.v | 22 +- theories/Sorting/Mergesort.v | 4 +- theories/Sorting/PermutEq.v | 2 +- theories/Sorting/PermutSetoid.v | 12 +- theories/Sorting/Permutation.v | 2 +- theories/Sorting/Sorted.v | 2 +- theories/Sorting/Sorting.v | 2 +- theories/Strings/Ascii.v | 16 +- theories/Strings/String.v | 130 +- theories/Structures/DecidableTypeEx.v | 6 +- theories/Structures/OrderedTypeEx.v | 160 +- theories/Structures/OrdersAlt.v | 6 +- theories/Unicode/Utf8.v | 4 +- theories/Unicode/Utf8_core.v | 2 +- theories/Vectors/VectorDef.v | 2 +- theories/Wellfounded/Disjoint_Union.v | 4 +- theories/Wellfounded/Inclusion.v | 4 +- theories/Wellfounded/Inverse_Image.v | 6 +- .../Wellfounded/Lexicographic_Exponentiation.v | 28 +- theories/Wellfounded/Lexicographic_Product.v | 10 +- theories/Wellfounded/Transitive_Closure.v | 6 +- theories/Wellfounded/Union.v | 6 +- theories/Wellfounded/Well_Ordering.v | 8 +- theories/Wellfounded/Wellfounded.v | 2 +- theories/ZArith/BinInt.v | 804 ++++---- theories/ZArith/BinIntDef.v | 253 +-- theories/ZArith/Int.v | 16 +- theories/ZArith/Wf_Z.v | 12 +- theories/ZArith/ZArith.v | 2 +- theories/ZArith/ZArith_base.v | 2 +- theories/ZArith/ZArith_dec.v | 93 +- theories/ZArith/Zabs.v | 56 +- theories/ZArith/Zbool.v | 16 +- theories/ZArith/Zcompare.v | 34 +- theories/ZArith/Zcomplements.v | 14 +- theories/ZArith/Zdigits.v | 58 +- theories/ZArith/Zdiv.v | 86 +- theories/ZArith/Zeuclid.v | 2 +- theories/ZArith/Zeven.v | 22 +- theories/ZArith/Zgcd_alt.v | 241 ++- theories/ZArith/Zhints.v | 95 +- theories/ZArith/Zlogarithm.v | 104 +- theories/ZArith/Zmax.v | 121 +- theories/ZArith/Zmin.v | 92 +- theories/ZArith/Zminmax.v | 16 +- theories/ZArith/Zmisc.v | 11 +- theories/ZArith/Znat.v | 162 +- theories/ZArith/Znumtheory.v | 385 ++-- theories/ZArith/Zorder.v | 100 +- theories/ZArith/Zpow_alt.v | 4 +- theories/ZArith/Zpow_def.v | 14 +- theories/ZArith/Zpow_facts.v | 42 +- theories/ZArith/Zpower.v | 14 +- theories/ZArith/Zquot.v | 351 ++-- theories/ZArith/Zsqrt_compat.v | 63 +- theories/ZArith/Zwf.v | 27 +- theories/ZArith/auxiliary.v | 2 +- tools/compat5.ml | 2 +- tools/compat5.mlp | 2 +- tools/compat5b.ml | 2 +- tools/compat5b.mlp | 2 +- tools/coq_makefile.ml | 6 +- tools/coq_tex.ml4 | 2 +- tools/coqdep.ml | 2 +- tools/coqdep_boot.ml | 2 +- tools/coqdep_common.ml | 2 +- tools/coqdep_common.mli | 2 +- tools/coqdep_lexer.mli | 2 +- tools/coqdep_lexer.mll | 2 +- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 2 +- tools/coqdoc/cpretty.mli | 2 +- tools/coqdoc/cpretty.mll | 71 +- tools/coqdoc/index.ml | 13 +- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 2 +- tools/coqdoc/output.ml | 151 +- tools/coqdoc/output.mli | 13 +- tools/coqdoc/tokens.ml | 2 +- tools/coqdoc/tokens.mli | 2 +- tools/coqwc.mll | 2 +- tools/escape_string.ml | 1 + tools/fake_ide.ml | 2 +- tools/gallina.ml | 2 +- tools/gallina_lexer.mll | 2 +- tools/mingwpath.ml | 15 + toplevel/auto_ind_decl.ml | 2 +- toplevel/auto_ind_decl.mli | 2 +- toplevel/autoinstance.ml | 2 +- toplevel/autoinstance.mli | 2 +- toplevel/backtrack.ml | 22 +- toplevel/backtrack.mli | 10 +- toplevel/cerrors.ml | 2 +- toplevel/cerrors.mli | 2 +- toplevel/class.ml | 2 +- toplevel/class.mli | 2 +- toplevel/classes.ml | 2 +- toplevel/classes.mli | 2 +- toplevel/command.ml | 9 +- toplevel/command.mli | 2 +- toplevel/coqinit.ml | 10 +- toplevel/coqinit.mli | 4 +- toplevel/coqtop.ml | 21 +- toplevel/coqtop.mli | 2 +- toplevel/discharge.ml | 2 +- toplevel/discharge.mli | 2 +- toplevel/himsg.ml | 57 +- toplevel/himsg.mli | 2 +- toplevel/ide_intf.ml | 43 +- toplevel/ide_intf.mli | 2 +- toplevel/ide_slave.ml | 45 +- toplevel/ide_slave.mli | 2 +- toplevel/ind_tables.ml | 2 +- toplevel/ind_tables.mli | 2 +- toplevel/indschemes.ml | 2 +- toplevel/indschemes.mli | 2 +- toplevel/interface.mli | 16 +- toplevel/lemmas.ml | 2 +- toplevel/lemmas.mli | 2 +- toplevel/libtypes.ml | 2 +- toplevel/libtypes.mli | 2 +- toplevel/metasyntax.ml | 20 +- toplevel/metasyntax.mli | 4 +- toplevel/mltop.ml4 | 135 +- toplevel/mltop.mli | 25 +- toplevel/record.ml | 2 +- toplevel/record.mli | 2 +- toplevel/search.ml | 2 +- toplevel/search.mli | 2 +- toplevel/toplevel.ml | 2 +- toplevel/toplevel.mli | 2 +- toplevel/usage.ml | 4 +- toplevel/usage.mli | 2 +- toplevel/vernac.ml | 39 +- toplevel/vernac.mli | 2 +- toplevel/vernacentries.ml | 141 +- toplevel/vernacentries.mli | 4 +- toplevel/vernacexpr.ml | 18 +- toplevel/vernacinterp.ml | 2 +- toplevel/vernacinterp.mli | 2 +- toplevel/whelp.ml4 | 2 +- toplevel/whelp.mli | 2 +- 1107 files changed, 21802 insertions(+), 18994 deletions(-) delete mode 100644 INSTALL.macosx create mode 100644 TODO delete mode 100644 config/Makefile.template create mode 100755 dev/macosify_accel.sh delete mode 100644 doc/refman/RefMan-sch.tex create mode 100644 test-suite/bugs/closed/shouldsucceed/2817.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2836.v create mode 100644 theories/Lists/SetoidPermutation.v create mode 100644 theories/Reals/Machin.v create mode 100644 theories/Reals/Ranalysis5.v create mode 100644 theories/Reals/Ranalysis_reg.v create mode 100644 theories/Reals/Ratan.v create mode 100644 theories/Reals/Rtrigo1.v create mode 100644 tools/escape_string.ml create mode 100644 tools/mingwpath.ml (limited to 'theories/Numbers/NatInt') diff --git a/.gitignore b/.gitignore index 32a40af6..e0be678c 100644 --- a/.gitignore +++ b/.gitignore @@ -63,11 +63,12 @@ doc/refman/csdp.cache doc/refman/trace doc/refman/Reference-Manual.pdf doc/refman/Reference-Manual.ps +doc/refman/Reference-Manual.html +doc/refman/Reference-Manual.out +doc/refman/Reference-Manual.sh doc/refman/cover.html doc/refman/styles.hva -doc/refman/Reference-Manual.html doc/common/version.tex -doc/refman/Reference-Manual.sh doc/refman/coqide-queries.eps doc/refman/coqide.eps doc/refman/euclid.ml diff --git a/CHANGES b/CHANGES index c245fb25..1c094584 100644 --- a/CHANGES +++ b/CHANGES @@ -1,29 +1,66 @@ -Changes from V8.4beta to V8.4 -============================= +Changes from V8.4beta2 to V8.4 +============================== + +Vernacular commands + +- The "Reset" command is now supported again in files given to coqc or Load. +- "Show Script" now indents again the displayed scripts. It can also work + correctly across Load'ed files if the option "Unset Atomic Load" is used. +- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full + scope name (e.g. Z_scope). + +Notations + +- Most compatibility notations of the standard library are now tagged as + (compat xyz), where xyz is a former Coq version, for instance "8.3". + These notations behave as (only parsing) notations, except that they may + triggers warnings (or errors) when used while Coq is not in a corresponding + -compat mode. +- To activate these compatibility warnings, use "Set Verbose Compat Notations" + or the command-line flag -verbose-compat-notations. +- For a strict mode without these compatibility notations, use + "Unset Compat Notations" or the command-line flag -no-compat-notations. + +Tactics + +- An annotation "eqn:H" or "eqn:?" can be added to a "destruct" + or "induction" to make it generate equations in the spirit of "case_eq". + The former syntax "_eqn" is discontinued. +- The name of the hypothesis introduced by tactic "remember" can be + set via the new syntax "remember t as x eqn:H" (wish #2489). + +Libraries + +- Reals: changed definition of PI, no more axiom about sin(PI/2). +- SetoidPermutation: a notion of permutation for lists modulo a setoid equality. +- BigN: fixed the ocaml code doing the parsing/printing of big numbers. + +Changes from V8.4beta to V8.4beta2 +================================== Vernacular commands -- Undo and UndoTo are now handling the proof states. They may - perform some extra steps of backtrack to avoid states where - the proof state is unavailable (typically a closed proof). -- The commands Suspend and Resume have been removed. +- Commands "Back" and "BackTo" are now handling the proof states. They may + perform some extra steps of backtrack to avoid states where the proof + state is unavailable (typically a closed proof). +- The commands "Suspend" and "Resume" have been removed. - A basic Show Script has been reintroduced (no indentation). - New command "Set Parsing Explicit" for deactivating parsing (and printing) of implicit arguments (useful for teaching). -- New command "Grab Existential Variables" to transform the unresolved evars at - the end of a proof into goals. +- New command "Grab Existential Variables" to transform the unresolved evars + at the end of a proof into goals. Tactics -- Still no general "info" tactical, but new specific tactics - info_auto, info_eauto, info_trivial which provides information - on the proofs found by auto/eauto/trivial. Display of these - details could also be activated by Set Info Auto/Eauto/Trivial. -- Details on everything tried by auto/eauto/trivial during - a proof search could be obtained by "debug auto", "debug eauto", - "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial". -- New command "r string" that interprets "idtac string" as a breakpoint - and jumps to its next use in Ltac debugger. +- Still no general "info" tactical, but new specific tactics info_auto, + info_eauto, info_trivial which provides information on the proofs found + by auto/eauto/trivial. Display of these details could also be activated by + "Set Info Auto"/"Set Info Eauto"/"Set Info Trivial". +- Details on everything tried by auto/eauto/trivial during a proof search + could be obtained by "debug auto", "debug eauto", "debug trivial" or by a + global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial". +- New command "r string" in Ltac debugger that interprets "idtac + string" in Ltac code as a breakpoint and jumps to its next use. - Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy) have been removed, since Why2 has not been maintained for the last few years. The Why3 plugin should be a suitable @@ -31,28 +68,28 @@ Tactics Libraries -- MSetRBT : a new implementation of MSets via Red-Black trees (initial +- MSetRBT: a new implementation of MSets via Red-Black trees (initial contribution by Andrew Appel). -- MSetAVL : for maximal sharing with the new MSetRBT, the argument order - of Node has changed (this should be transparent to regular MSets users). +- MSetAVL: for maximal sharing with the new MSetRBT, the argument order + of Node has changed (this should be transparent to regular MSets users). Module System - The names of modules (and module types) are now in a fully separated - namespace from ordinary definitions : "Definition E:=0. Module E. End E." + namespace from ordinary definitions: "Definition E:=0. Module E. End E." is now accepted. CoqIDE -- Coqide now supports the Restart command, and Undo (with a warning). - Better support for Abort. +- Coqide now supports the "Restart" command, and "Undo" (with a warning). + Better support for "Abort". Changes from V8.3 to V8.4beta ============================= Logic -- Standard eta-conversion now supported (dependent product only). (DOC TO DO) +- Standard eta-conversion now supported (dependent product only). - Guard condition improvement: subterm property is propagated through beta-redex blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x"; this allows for instance to use "rewrite ... in ..." without breaking @@ -69,10 +106,6 @@ Specification language and notations - Structure/Record printing can be disable by "Unset Printing Records". In addition, it can be controlled on type by type basis using "Add Printing Record" or "Add Printing Constructor". -- In a pattern containing a "match", a final "| _ => _" branch could be used - now instead of enumerating all remaining constructors. Moreover, the pattern - "match _ with _ => _ end" now allows to match any "match". A "in" annotation - can also be added to restrict to a precise inductive type. - Pattern-matching compilation algorithm: in "match x, y with ... end", possible dependencies of x (or of the indices of its type) in the type of y are now taken into account. @@ -81,11 +114,11 @@ Tactics - New proof engine. - Scripts can now be structured thanks to bullets - * + and to subgoal - delimitation via { }. Note: for use with ProofGeneral, a cvs version of - ProofGeneral no older than mid-July 2011 is currently required. DOC TODO. + delimitation via { }. Note: for use with Proof General, a cvs version of + Proof General no older than mid-July 2011 is currently required. - Support for tactical "info" is suspended. - Support for command "Show Script" is suspended. -- New tactics constr_eq, is_evar and has_evar. +- New tactics constr_eq, is_evar and has_evar for use in Ltac. - Removed the two-argument variant of "decide equality". - New experimental tactical "timeout ". Since is a time in second for the moment, this feature should rather be avoided @@ -98,14 +131,14 @@ Tactics ?f x y = g(x,y) (compatibility ensured by using "Unset Tactic Pattern Unification"). It also supports (full) betaiota. - Tactic autorewrite does no longer instantiate pre-existing - existential variables (theoretical source of possible incompatibility). + existential variables (theoretical source of possible incompatibilities). - Tactic "dependent rewrite" now supports equality in "sig". - Tactic omega now understands Zpred (wish #1912) and can prove any goal from a context containing an arithmetical contradiction (wish #2236). - Using "auto with nocore" disables the use of the "core" database (wish #2188). This pseudo-database "nocore" can also be used with trivial and eauto. - Tactics "set", "destruct" and "induction" accepts incomplete terms and - use the goal to complete the pattern assuming it is no ambiguous. + use the goal to complete the pattern assuming it is non ambiguous. - When used on arguments with a dependent type, tactics such as "destruct", "induction", "case", "elim", etc. now try to abstract automatically the dependencies over the arguments of the types @@ -118,18 +151,25 @@ Tactics - When applying destruct or inversion on a fixpoint hiding an inductive type, recursive calls to the fixpoint now remain folded by default (rare source of incompatibility generally solvable by adding a call to simpl). -- The behavior of the simpl tactic can be tuned using the new "Arguments" - vernacular. +- In an ltac pattern containing a "match", a final "| _ => _" branch could be + used now instead of enumerating all remaining constructors. Moreover, the + pattern "match _ with _ => _ end" now allows to match any "match". A "in" + annotation can also be added to restrict to a precise inductive type. +- The behavior of "simpl" can be tuned using the "Arguments" vernacular. + In particular constants can be marked so that they are always/never unfolded + by "simpl", or unfolded only when a set of arguments evaluates to a + constructor. Last one can mark a constant so that it is unfolded only if the + simplified term does not expose a match in head position. Vernacular commands - It is now mandatory to have a space (or tabulation or newline or end-of-file) after a "." ending a sentence. - In SearchAbout, the [ ] delimiters are now optional. -- New command "Add/Remove Search Blacklist ..." : +- New command "Add/Remove Search Blacklist ...": a Search or SearchAbout or similar query will never mention lemmas whose qualified names contain any of the declared substrings. - The default blacklisted substrings are "_admitted" "_subproof" "Private_". DOC TODO + The default blacklisted substrings are "_admitted" "_subproof" "Private_". - When the output file of "Print Universes" ends in ".dot" or ".gv", the universe graph is printed in the DOT language, and can be processed by Graphviz tools. @@ -141,7 +181,11 @@ Vernacular commands to avoid conversion at Qed time to go into a very long computation. - New command "Show Goal ident" to display the statement of a goal, even a closed one (available from Proof General). -- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope". +- Command "Proof" accept a new modifier "using" to force generalization + over a given list of section variables at section ending. +- New command "Arguments" generalizing "Implicit Arguments" and + "Arguments Scope" and that also allows to rename the parameters of a + definition and to tune the behavior of the tactic "simpl". Module System @@ -155,8 +199,8 @@ Module System are lower or equal than XX will be inlined. The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use - the flag "Set Inline Level ..." to set a level. TODO: DOC! -- Print Assumptions should now handle correctly opaque modules (#2168) + the flag "Set Inline Level ..." to set a level. +- Print Assumptions should now handle correctly opaque modules (#2168). - Print Module (Type) now tries to print more details, such as types and bodies of the module elements. Note that Print Module Type could be used on a module to display only its interface. The option @@ -166,9 +210,9 @@ Module System Libraries - Extension of the abstract part of Numbers, which now provide axiomatizations - and results about many more integer functions, such as pow, gcd, lcm, sqrt, log2 - and bitwise functions. These functions are implemented for nat N BigN Z BigZ. - See in particular file NPeano for new functions about nat. + and results about many more integer functions, such as pow, gcd, lcm, sqrt, + log2 and bitwise functions. These functions are implemented for nat, N, BigN, + Z, BigZ. See in particular file NPeano for new functions about nat. - The definition of types positive, N, Z is now in file BinNums.v - Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains an internal module Z implementing the Numbers interface for integers. @@ -207,15 +251,15 @@ Libraries may introduce incompatibilities. In particular, the order of the arguments for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now comes first. By default, the power function now takes two BigN. -- Creation of Vector, an independant library for list indiced by their length. - Vectors' names overwrite lists' one so you shouldn't "Import" the library. - All old names change: functions' name become the CaML one and for example - Vcons become Vector.cons. You can use notations by importing +- Creation of Vector, an independent library for lists indexed by their length. + Vectors' names overwrite lists' one so you should not "Import" the library. + All old names changed: function names follow the ocaml ones and, for example, + Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing Vector.VectorNotations. - Removal of TheoryList. Requiring List instead should work most of the time. -- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and +- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and eq_rect_r (available by importing module EqNotations). -- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument) +- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument). Internal infrastructure @@ -230,8 +274,8 @@ Internal infrastructure for both make and ocamlbuild, etc. - Support of cross-compilation via mingw from unix toward Windows, contact P. Letouzey for more informations. -- new Makefile rules mli-doc to make html of mli in dev/doc/html and - full-stdlib to get a HUGE pdf with all the stdlib. +- New Makefile rules mli-doc to make html of mli in dev/doc/html and + full-stdlib to get a (huge) pdf reflecting the whole standard library. Extraction @@ -243,9 +287,8 @@ Extraction - A new command "Separate Extraction cst1 cst2 ..." that mixes a minimal extracted environment a la "Recursive Extraction" and the production of several files (one per coq source) a la "Extraction Library". - DOC TODO. - New option "Set/Unset Extraction KeepSingleton" for preventing the - extraction to optimize singleton container types. DOC TODO + extraction to optimize singleton container types. - The extraction now identifies and properly rejects a particular case of universe polymorphism it cannot handle yet (the pair (I,I) being Prop). - Support of anonymous fields in record (#2555). @@ -257,10 +300,9 @@ CoqIDE (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts, the Windows version of coqide now requires Windows >= XP SP1. -- The communication between CoqIDE and Coqtop is now done via a dialect - of XML (DOC TODO). -- The backtrack engine of CoqIDE has been reworked, it now used the - "Backtrack" command similarly to ProofGeneral. +- The communication between CoqIDE and Coqtop is now done via a dialect of XML. +- The backtrack engine of CoqIDE has been reworked, it now uses the + "Backtrack" command similarly to Proof General. - The Coqide parsing of sentences has be reworked and now supports tactic delimitation via { }. - Coqide now accepts the Abort command (wish #2357). @@ -274,15 +316,15 @@ Tools - Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq, $XDG_DATA_DIRS/coq, and user-contribs before the standard library. - Coq rc file has moved to $XDG_CONFIG_HOME/coq. -- coq_makefile major cleanup. - * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work +- Major changes to coq_makefile: + * mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work; * mlihtml generates doc of mli, install-doc install the html doc in DOCDIR - with the same policy as vo in COQLIB + with the same policy as vo in COQLIB; * More variables are given by coqtop -config, others are defined only if the users doesn't have defined them elsewhere. Consequently, generated makefile - should work directly on any architecture. + should work directly on any architecture; * Packagers can take advantage of $(DSTROOT) introduction. Installation can - be made in $XDG_DATA_HOME/coq. + be made in $XDG_DATA_HOME/coq; * -arg option allows to send option as argument to coqc. Changes from V8.2 to V8.3 diff --git a/COMPATIBILITY b/COMPATIBILITY index 0849b64f..41474202 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -3,4 +3,49 @@ Potential sources of incompatibilities between Coq V8.3 and V8.4 (see also file CHANGES) -TO BE DONE +The main known incompatibilities between 8.3 and 8.4 are consequences +of the following changes: + +- The reorganization of the library of numbers: + + Several definitions have new names or are defined in modules of + different names, but a special care has been taken to have this + renaming transparent for the user thanks to compatibility notations. + + However some definitions have changed, what might require some + adaptations. The most noticeable examples are: + - The "?=" notation which now bind to Pos.compare rather than former + Pcompare (now Pos.compare_cont). + - Changes in names may induce different automatically generated + names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec"). + - Z.add has a new definition, hence, applying "simpl" on subterms of + its body might give different results than before. + - BigN.shiftl and BigN.shiftr have reversed arguments order, the + power function in BigN now takes two BigN. + +- Other changes in libraries: + + - The definition of functions over "vectors" (list of fixed length) + have changed. + - TheoryList.v has been removed. + +- Slight changes in tactics: + + - Less unfolding of fixpoints when applying destruct or inversion on + a fixpoint hiding an inductive type (add an extra call to simpl to + preserve compatibility). + - Less unexpected local definitions when applying "destruct" + (incompatibilities solvable by adapting name hypotheses). + - Tactic "apply" might succeed more often, e.g. by now solving + pattern-matching of the form ?f x y = g(x,y) (compatibility + ensured by using "Unset Tactic Pattern Unification"), but also + because it supports (full) betaiota (using "simple apply" might + then help). + - Tactic autorewrite does no longer instantiate pre-existing + existential variables. + - Tactic "info" is now available only for auto, eauto and trivial. + +- Miscellaneous changes: + + - The command "Load" is now atomic for backtracking (use "Unset + Atomic Load" for compatibility). diff --git a/INSTALL b/INSTALL index 5ee00613..02c9eb9b 100644 --- a/INSTALL +++ b/INSTALL @@ -1,5 +1,5 @@ - INSTALLATION PROCEDURES FOR THE COQ V8.3 SYSTEM + INSTALLATION PROCEDURES FOR THE COQ V8.4 SYSTEM ----------------------------------------------- diff --git a/INSTALL.macosx b/INSTALL.macosx deleted file mode 100644 index cc1317b1..00000000 --- a/INSTALL.macosx +++ /dev/null @@ -1,20 +0,0 @@ -INSTALLATION PROCEDURE FOR THE PRECOMPILED COQ V8.1 SYSTEM UNDER MACOS X ------------------------------------------------------------------------- - -You can also use fink, or the MacOS X package prepared by the Coq -team. To use the MacOS X package,: - -1) Download archive coq-8.1-macosx-ppc.dmg (for PowerPC-base computer) - or coq-8.1-macosx-i386.dmg (for Pentium-based computer). - -2) Double-click on its icon; it mounts a disk volume named "Coq V8.1". - -3) Open volume "Coq 8.1" and double-click on coq-8.1.pkg to launch the - installer (you'll need administrator permissions). - -4) Coq installs in /usr/local/bin, which should be in your PATH, and - can be used from a Terminal window: the interactive toplevel is - named coqtop and the compiler is coqc. - -If you have any trouble with this installation, please contact: -coq-bugs@pauillac.inria.fr. diff --git a/Makefile b/Makefile index 0ff72856..bb5ec3bc 100644 --- a/Makefile +++ b/Makefile @@ -39,9 +39,13 @@ # File lists ########################################################################### +# NB: due to limitations in Win32, please refrain using 'export' too much +# to communicate between make sub-calls (in Win32, 8kb max per env variable, +# 32kb total) + # !! Before using FIND_VCS_CLAUSE, please read how you should in the !! # !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !! -export FIND_VCS_CLAUSE:='(' \ +FIND_VCS_CLAUSE:='(' \ -name '{arch}' -o \ -name '.svn' -o \ -name '_darcs' -o \ @@ -58,8 +62,8 @@ endef ## Files in the source tree -export YACCFILES:=$(call find, '*.mly') -export LEXFILES := $(call find, '*.mll') +YACCFILES:=$(call find, '*.mly') +LEXFILES := $(call find, '*.mll') export MLLIBFILES := $(call find, '*.mllib') export ML4FILES := $(call find, '*.ml4') export CFILES := $(call find, '*.c') @@ -73,13 +77,13 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ +GENML4FILES:= $(ML4FILES:.ml4=.ml) +GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ scripts/tolink.ml kernel/copcodes.ml -export GENMLIFILES:=$(YACCFILES:.mly=.mli) +GENMLIFILES:=$(YACCFILES:.mly=.mli) +GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v -export GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) -export GENML4FILES:= $(ML4FILES:.ml4=.ml) export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD) # NB: all files in $(GENFILES) can be created initially, while @@ -92,12 +96,9 @@ define diff $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) endef -export MLSTATICFILES := \ - $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)) -export MLFILES := \ - $(sort $(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)) +export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD) +export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES)) export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) -export MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml)) include Makefile.common @@ -276,3 +277,14 @@ ifdef COQ_CONFIGURED else @echo "Please run ./configure first" >&2; exit 1 endif + +# Useful to check that the exported variables are within the win32 limits + +printenv: + @env + @echo + @echo -n "Maxsize (win32 limit is 8k) : " + @env | wc -L + @echo -n "Total (win32 limit is 32k) : " + @env | wc -m + diff --git a/Makefile.build b/Makefile.build index 41dfabbf..fe99f3b0 100644 --- a/Makefile.build +++ b/Makefile.build @@ -36,10 +36,12 @@ endif # of include, and they will then be automatically deleted, leading to an # infinite loop. -ALLDEPS=$(addsuffix .d, \ +MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES) + +ALLDEPS:=$(addsuffix .d, \ $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES)) -.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES) +.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml) # NOTA: the -include below will lauch the build of all .d. Some of them # will _fail_ at first, this is to be expected (no grammar.cma initially). @@ -82,12 +84,15 @@ HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) +COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB) OCAMLC += $(CAMLFLAGS) OCAMLOPT += $(CAMLFLAGS) BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) +COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) +COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= -slash $(LOCALINCLUDES) define bestocaml @@ -96,7 +101,7 @@ $(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\ $(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^) endef -CAMLP4DEPS=`sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<` +CAMLP4DEPS=`LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<` ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) else @@ -169,10 +174,12 @@ CINCLUDES= -I $(CAMLHLIB) # libcoqrun.a, dllcoqrun.so +# NB: We used to do a ranlib after ocamlmklib, but it seems that +# ocamlmklib is already doing it + $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u))) - $(RANLIB) $(LIBCOQRUN) #coq_jumptbl.h is required only if you have GCC 2.0 or later kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h @@ -201,12 +208,12 @@ states:: states/initial.coq $(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@ $(STRIP) $@ $(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@ $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) @@ -544,9 +551,9 @@ $(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BEST ifeq ($(CAMLP4),camlp4) tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< else tools/compat5.cmo: tools/compat5.ml $(OCAMLC) -c $< @@ -729,7 +736,7 @@ dev/printers.cma: | dev/printers.mllib.d parsing/grammar.cma: | parsing/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ @@ -846,6 +853,12 @@ COND_OPTFLAGS= \ HACKMLI = $(if $(wildcard $) + +Theories: + +- Rendre transparent tous les theoremes prouvant {A}+{B} +- Faire demarrer PolyList.nth a` l'indice 0 + Renommer l'actuel nth en nth1 ?? + +Doc: + +- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection +- Documenter le filtrage sur les types inductifs avec let-ins (dont la + compatibilite V6) + +- Ajouter let dans les règles du CIC + -> FAIT, mais reste a documenter le let dans les inductifs + et les champs manifestes dans les Record +- revoir le chapitre sur les tactiques utilisateur +- faut-il mieux spécifier la sémantique de Simpl (??) + +- Préciser la clarification syntaxique de IntroPattern +- preciser que Goal vient en dernier dans une clause pattern list et + qu'il doit apparaitre si il y a un "in" + +- Omega Time debranche mais Omega System et Omega Action remarchent ? +- Ajout "Replace in" (mais TODO) +- Syntaxe Conditional tac Rewrite marche, à documenter +- Documenter Dependent Rewrite et CutRewrite ? +- Ajouter les motifs sous-termes de ltac + +- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) +- mettre à jour la doc de induction (arguments multiples) (Pierre C.) +- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) +--> mettre à jour le CHANGES (vers la ligne 72) + + diff --git a/checker/check.ml b/checker/check.ml index bb42b949..237eb079 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* " - echo "-with-ar " - echo "-with-ranlib " - printf "\tTells configure where to find gcc/ar/ranlib executables\n" echo "-byte-only" printf "\tCompiles only bytecode version of Coq\n" echo "-debug" @@ -119,10 +115,6 @@ best_compiler=opt cflags="-fno-defer-pop -Wall -Wno-unused" natdynlink=yes -gcc_exec=gcc -ar_exec=ar -ranlib_exec=ranlib - local=false coqrunbyteflags_spec=no coqtoolsbyteflags_spec=no @@ -254,18 +246,6 @@ while : ; do no) with_geoproof=false;; esac shift;; - -with-cc|-with-gcc|--with-cc|--with-gcc) - gcc_spec=yes - gcc_exec=$2 - shift;; - -with-ar|--with-ar) - ar_spec=yes - ar_exec=$2 - shift;; - -with-ranlib|--with-ranlib) - ranlib_spec=yes - ranlib_exec=$2 - shift;; -makecmd|--makecmd) makecmd="$2" shift;; -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;; @@ -292,17 +272,19 @@ case $DATEPGM in "") echo "I can't find the program \"date\" in your path." echo "Please give me the current date" read COMPILEDATE;; - *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;; + *) COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;; esac # Architecture case $arch_spec in no) - # First we test if we are running a Cygwin system + # First we test if we are running a Cygwin or Mingw/Msys system if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then ARCH="win32" CYGWIN=yes + elif [ `uname -s | cut -c -7` = "MINGW32" ]; then + ARCH="win32" else # If not, we determine the architecture if test -x /bin/uname ; then @@ -437,12 +419,26 @@ if test ! -f "$CAMLC" ; then exit 1 fi -# Under Windows, OCaml only understands Windows filenames (C:\...) -case $ARCH in - win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;; +# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml) +# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept + +mk_win_path () { + case $ARCH,$CYGWIN in + win32,yes) cygpath -m "$1" ;; + win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;; + *) echo "$1" ;; + esac +} + +case $ARCH,$src_spec in + win32,yes) echo "Error: the -src option is currently not supported on Windows" + exit 1;; + win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;; esac -CAMLVERSION=`"$bytecamlc" -version` +# Beware of the final \r in Win32 +CAMLVERSION=`"$CAMLC" -version | tr -d "\r"` +CAMLLIB=`"$CAMLC" -where | tr -d "\r"` case $CAMLVERSION in 1.*|2.*|3.0*|3.10*|3.11.[01]) @@ -454,7 +450,7 @@ case $CAMLVERSION in echo " Configuration script failed!" exit 1 fi;; - 3.11.2|3.12*) + 3.11.2|3.12*|4.*) CAMLP4COMPAT="-loc loc" echo "You have Objective-Caml $CAMLVERSION. Good!";; *) @@ -468,16 +464,9 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` # For coqmktop & bytecode compiler -case $ARCH in - win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB - CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;; - *) - CAMLLIB=`"$CAMLC" -where` -esac - if [ "$coq_debug_flag" = "-g" ]; then case $CAMLTAG in - OCAML31*) + OCAML31*|OCAML4*) # Compilation debug flag coq_debug_flag_opt="-g" ;; @@ -485,7 +474,7 @@ if [ "$coq_debug_flag" = "-g" ]; then fi # Native dynlink -if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then +if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then HASNATDYNLINK=true else HASNATDYNLINK=false @@ -520,7 +509,8 @@ esac # (this should become configurable some day) CAMLP4BIN=${CAMLBIN} -if [ "$usecamlp5" = "yes" ]; then +case $usecamlp5 in + yes) CAMLP4=camlp5 CAMLP4MOD=gramlib if [ "$camlp5dir" != "" ]; then @@ -539,38 +529,47 @@ if [ "$usecamlp5" = "yes" ]; then CAMLP4LIB=+site-lib/camlp5 FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5 else - echo "Objective Caml $CAMLVERSION found but no Camlp5 installed." - echo "Configuration script failed!" - exit 1 + echo "No Camlp5 installation found. Looking for Camlp4 instead..." + usecamlp5=no fi +esac - camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` - case `$camlp4oexec -v 2>&1` in - *4.0*|*5.00*) +# If we're (still...) going to use Camlp5, let's check its version + +case $usecamlp5 in + yes) + camlp4oexec=`echo "$camlp4oexec" | tr 4 5` + case `"$camlp4oexec" -v 2>&1` in + *"version 4.0"*|*5.00*) echo "Camlp5 version < 5.01 not supported." echo "Configuration script failed!" exit 1;; esac +esac + +# We might now try to use Camlp4, either by explicit choice or +# by lack of proper Camlp5 installation -else # let's use camlp4 +case $usecamlp5 in + no) CAMLP4=camlp4 CAMLP4MOD=camlp4lib CAMLP4LIB=+camlp4 FULLCAMLP4LIB=${CAMLLIB}/camlp4 if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then - echo "Objective Caml $CAMLVERSION found but no Camlp4 installed." + echo "No Camlp4 installation found." echo "Configuration script failed!" exit 1 fi camlp4oexec=${camlp4oexec}rf - if [ "`$camlp4oexec 2>&1`" != "" ]; then + if [ "`"$camlp4oexec" 2>&1`" != "" ]; then echo "Error: $camlp4oexec not found or not executable." echo "Configuration script failed!" exit 1 fi -fi +esac # do we have a native compiler: test of ocamlopt and its version @@ -595,18 +594,17 @@ fi # OS dependent libraries -case $ARCH in +OSDEPLIBS="-cclib -lunix" +case $ARCH,$CYGWIN in sun4*) OS=`uname -r` case $OS in 5*) OS="Sun Solaris $OS" - OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";; + OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";; *) OS="Sun OS $OS" - OSDEPLIBS="-cclib -lunix" esac;; - win32) OS="Win32" - OSDEPLIBS="-cclib -lunix" + win32,yes) OS="Win32 (Cygwin)" cflags="-mno-cygwin $cflags";; - *) OSDEPLIBS="-cclib -lunix" + win32,*) OS="Win32 (MinGW)";; esac # lablgtk2 and CoqIDE @@ -628,11 +626,11 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then echo "CoqIde disabled as requested." else case $lablgtkdir_spec in - no) - if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then + no) + if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then + lablgtkdir_spec=yes + elif [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then lablgtkdir=${CAMLLIB}/lablgtk2 - elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then - lablgtkdir=${CAMLLIB}/site-lib/lablgtk2 fi;; yes) if [ ! -f "$lablgtkdir/glib.mli" ]; then @@ -656,10 +654,10 @@ else else echo "LablGtk2 found, native threads: native CoqIde will be available." COQIDE=opt - if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration; + if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration; then - cflags=$cflags" `pkg-config --cflags ige-mac-integration`" - IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"' + cflags=$cflags" `pkg-config --cflags gtk-mac-integration`" + IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"' IDEARCHFILE=ide/ide_mac_stubs.o IDEARCHDEF=QUARTZ elif [ "$ARCH" = "win32" ]; @@ -685,9 +683,6 @@ esac # strip command case $ARCH in - win32) - # true -> strip : it exists under cygwin ! - STRIPCOMMAND="strip";; Darwin) if [ "$HASNATDYNLINK" = "true" ] then STRIPCOMMAND="true" @@ -703,13 +698,6 @@ case $ARCH in fi esac -# mktexlsr -#MKTEXLSR=`which mktexlsr` -#case $MKTEXLSR in -# "") MKTEXLSR=true;; -#esac - -# " ### Test if documentation can be compiled (latex, hevea) if test "$with_doc" = "all" @@ -727,26 +715,28 @@ fi ########################################### # bindir, libdir, mandir, docdir, etc. -case $src_spec in - no) COQTOP=${COQSRC} -esac - # OCaml only understand Windows filenames (C:\...) case $ARCH in - win32) COQTOP=`cygpath -m ${COQTOP}` + win32) COQSRC=`mk_win_path "$COQSRC"` + CAMLBIN=`mk_win_path "$CAMLBIN"` + CAMLP4BIN=`mk_win_path "$CAMLP4BIN"` +esac + +case $src_spec in + no) COQTOP=${COQSRC} esac case $ARCH$CYGWIN in win32) - W32PREF='C:\\coq\\' - bindir_def=${W32PREF}bin - libdir_def=${W32PREF}lib - configdir_def=${W32PREF}config - datadir_def=${W32PREF}share - mandir_def=${W32PREF}man - docdir_def=${W32PREF}doc - emacslib_def=${W32PREF}emacs - coqdocdir_def=${W32PREF}latex;; + W32PREF='C:\coq\' + bindir_def="${W32PREF}bin" + libdir_def="${W32PREF}lib" + configdir_def="${W32PREF}config" + datadir_def="${W32PREF}share" + mandir_def="${W32PREF}man" + docdir_def="${W32PREF}doc" + emacslib_def="${W32PREF}emacs" + coqdocdir_def="${W32PREF}latex";; *) bindir_def=/usr/local/bin libdir_def=/usr/local/lib/coq @@ -755,7 +745,7 @@ case $ARCH$CYGWIN in mandir_def=/usr/local/share/man docdir_def=/usr/local/share/doc/coq emacslib_def=/usr/local/share/emacs/site-lisp - coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;; + coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;; esac emacs_def=emacs @@ -764,7 +754,7 @@ case $bindir_spec/$prefix_spec/$local in yes/*/*) BINDIR=$bindir ;; */yes/*) BINDIR=$prefix/bin ;; */*/true) BINDIR=$COQTOP/bin ;; - *) printf "Where should I install the Coq binaries [$bindir_def]? " + *) printf "Where should I install the Coq binaries [%s]? " "$bindir_def" read BINDIR case $BINDIR in "") BINDIR=$bindir_def;; @@ -781,7 +771,7 @@ case $libdir_spec/$prefix_spec/$local in *) LIBDIR=$prefix/lib/coq ;; esac ;; */*/true) LIBDIR=$COQTOP ;; - *) printf "Where should I install the Coq library [$libdir_def]? " + *) printf "Where should I install the Coq library [%s]? " "$libdir_def" read LIBDIR libdir_spec=yes case $LIBDIR in @@ -790,11 +780,6 @@ case $libdir_spec/$prefix_spec/$local in esac;; esac -case $libdir_spec in - yes) LIBDIR_OPTION="Some \"$LIBDIR\"";; - *) LIBDIR_OPTION="None";; -esac - case $configdir_spec/$prefix_spec/$local in yes/*/*) CONFIGDIR=$configdir;; */yes/*) configdir_spec=yes @@ -804,7 +789,7 @@ case $configdir_spec/$prefix_spec/$local in esac;; */*/true) CONFIGDIR=$COQTOP/ide configdir_spec=yes;; - *) printf "Where should I install the Coqide configuration files [$configdir_def]? " + *) printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def" read CONFIGDIR case $CONFIGDIR in "") CONFIGDIR=$configdir_def;; @@ -812,17 +797,12 @@ case $configdir_spec/$prefix_spec/$local in esac;; esac -case $configdir_spec in - yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";; - *) CONFIGDIR_OPTION="None";; -esac - case $datadir_spec/$prefix_spec/$local in yes/*/*) DATADIR=$datadir;; */yes/*) DATADIR=$prefix/share/coq;; */*/true) DATADIR=$COQTOP/ide datadir_spec=yes;; - *) printf "Where should I install the Coqide data files [$datadir_def]? " + *) printf "Where should I install the Coqide data files [%s]? " "$datadir_def" read DATADIR case $DATADIR in "") DATADIR=$datadir_def;; @@ -830,17 +810,11 @@ case $datadir_spec/$prefix_spec/$local in esac;; esac -case $datadir_spec in - yes) DATADIR_OPTION="Some \"$DATADIR\"";; - *) DATADIR_OPTION="None";; -esac - - case $mandir_spec/$prefix_spec/$local in yes/*/*) MANDIR=$mandir;; */yes/*) MANDIR=$prefix/share/man ;; */*/true) MANDIR=$COQTOP/man ;; - *) printf "Where should I install the Coq man pages [$mandir_def]? " + *) printf "Where should I install the Coq man pages [%s]? " "$mandir_def" read MANDIR case $MANDIR in "") MANDIR=$mandir_def;; @@ -852,7 +826,7 @@ case $docdir_spec/$prefix_spec/$local in yes/*/*) DOCDIR=$docdir;; */yes/*) DOCDIR=$prefix/share/doc/coq;; */*/true) DOCDIR=$COQTOP/doc;; - *) printf "Where should I install the Coq documentation [$docdir_def]? " + *) printf "Where should I install the Coq documentation [%s]? " "$docdir_def" read DOCDIR case $DOCDIR in "") DOCDIR=$docdir_def;; @@ -868,7 +842,7 @@ case $emacslib_spec/$prefix_spec/$local in *) EMACSLIB=$prefix/share/emacs/site-lisp ;; esac ;; */*/true) EMACSLIB=$COQTOP/tools/emacs ;; - *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? " + *) printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def" read EMACSLIB case $EMACSLIB in "") EMACSLIB=$emacslib_def;; @@ -884,7 +858,7 @@ case $coqdocdir_spec/$prefix_spec/$local in *) COQDOCDIR=$prefix/share/emacs/site-lisp ;; esac ;; */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;; - *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? " + *) printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def" read COQDOCDIR case $COQDOCDIR in "") COQDOCDIR=$coqdocdir_def;; @@ -914,14 +888,14 @@ case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in esac # case $emacs_spec in -# no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? " +# no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def" # read EMACS # case $EMACS in -# "") EMACS=$emacs_def;; +# "") EMACS="$emacs_def";; # *) true;; # esac;; -# yes) EMACS=$emacs;; +# yes) EMACS="$emacs";; # esac @@ -1016,51 +990,63 @@ config_template="$COQSRC/config/Makefile.template" ### After this line, be careful when using variables, ### since some of them (e.g. $COQSRC) will be escaped - -# An escaped version of a variable -escape_var () { -"$ocamlexec" 2>&1 1>/dev/null < "$config_file" +cat << END_OF_MAKEFILE > $config_file +###### config/Makefile : Configuration file for Coq ############## +# # +# This file is generated by the script "configure" # +# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! # +# If something is wrong below, then rerun the script "configure" # +# with the good options (see the file INSTALL). # +# # +################################################################## + +#Variable used to detect whether ./configure has run successfully. +COQ_CONFIGURED=yes + +# Local use (no installation) +LOCAL=$local + +# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun") +COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS +COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS +$BUILDLDPATH + +# Paths for true installation +# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and +# do_Makefile will reside +# LIBDIR=path where the Coq library will reside +# MANDIR=path where to install manual pages +# EMACSDIR=path where to put Coq's Emacs mode (coq.el) +BINDIR="$BINDIR" +COQLIBINSTALL="$LIBDIR" +CONFIGDIR="$CONFIGDIR" +DATADIR="$DATADIR" +MANDIR="$MANDIR" +DOCDIR="$DOCDIR" +EMACSLIB="$EMACSLIB" +EMACS=$EMACS + +# Path to Coq distribution +COQSRC="$COQSRC" +VERSION=$VERSION + +# Ocaml version number +CAMLVERSION=$CAMLTAG + +# Ocaml libraries +CAMLLIB="$CAMLLIB" + +# Ocaml .h directory +CAMLHLIB="$CAMLLIB" + +# Camlp4 : flavor, binaries, libraries ... +# NB : CAMLP4BIN can be empty if camlp4 is in the PATH +# NB : avoid using CAMLP4LIB (conflict under Windows) +CAMLP4BIN="$CAMLP4BIN" +CAMLP4=$CAMLP4 +CAMLP4O=$camlp4oexec +CAMLP4COMPAT=$CAMLP4COMPAT +MYCAMLP4LIB="$CAMLP4LIB" + +# LablGTK +COQIDEINCLUDES=$LABLGTKINCLUDES + +# Objective-Caml compile command +OCAML="$ocamlexec" +OCAMLC="$bytecamlc" +OCAMLMKLIB="$ocamlmklibexec" +OCAMLOPT="$nativecamlc" +OCAMLDEP="$ocamldepexec" +OCAMLDOC="$ocamldocexec" +OCAMLLEX="$ocamllexexec" +OCAMLYACC="$ocamlyaccexec" + +# Caml link command and Caml make top command +CAMLLINK="$bytecamlc" +CAMLOPTLINK="$nativecamlc" +CAMLMKTOP="$ocamlmktopexec" + +# Caml flags +CAMLFLAGS=-rectypes $coq_annotate_flag + +# Compilation debug flags +CAMLDEBUG=$coq_debug_flag +CAMLDEBUGOPT=$coq_debug_flag_opt + +# User compilation flag +USERFLAGS= + +# Flags for GCC +CFLAGS=$cflags + +# Compilation profile flag +CAMLTIMEPROF=$coq_profile_flag + +# The best compiler: native (=opt) or bytecode (=byte) if no native compiler +BEST=$best_compiler + +# Your architecture +# Can be obtain by UNIX command arch +ARCH=$ARCH +HASNATDYNLINK=$NATDYNLINKFLAG + +# Supplementary libs for some systems, currently: +# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket +# . others : -cclib -lunix +OSDEPLIBS=$OSDEPLIBS + +# executable files extension, currently: +# Unix systems: +# Win32 systems : .exe +EXE=$EXE +DLLEXT=$DLLEXT + +# the command MKDIR (try to replace it with mkdirhier if you have problems) +MKDIR=mkdir -p + +# where to put the coqdoc.sty style file +COQDOCDIR="$COQDOCDIR" + +#the command STRIP +# Unix systems and profiling: true +# Unix systems and no profiling: strip +STRIP=$STRIPCOMMAND + +# CoqIde (no/byte/opt) +HASCOQIDE=$COQIDE +IDEOPTFLAGS=$IDEARCHFLAGS +IDEOPTDEPS=$IDEARCHFILE +IDEOPTINT=$IDEARCHDEF + +# Defining REVISION +CHECKEDOUT=$checkedout + +# Option to control compilation and installation of the documentation +WITHDOC=$with_doc + +# make or sed are bogus and believe lines not terminating by a return +# are inexistent +END_OF_MAKEFILE chmod a-w "$config_file" diff --git a/dev/db_printers.ml b/dev/db_printers.ml index b3edd7d0..f54df8a8 100644 --- a/dev/db_printers.ml +++ b/dev/db_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* \(.*\)$/\1\2/ +s/^;\{0,1\} *\(.*\)\(.*\)$/\1\2/ diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3116cbf2..0038e78a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* try pp(pr_ltype x) with e -> pp (str (Printexc.to_string let ppfconstr c = ppconstr (Closure.term_of_fconstr c) -let ppbigint n = pp (Bigint.pr_bigint n);; +let ppbigint n = pp (str (Bigint.to_string n));; let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Intset.elements l)) diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex deleted file mode 100644 index 707ee824..00000000 --- a/doc/refman/RefMan-sch.tex +++ /dev/null @@ -1,418 +0,0 @@ -\chapter{Proof schemes} - -\section{Generation of induction principles with {\tt Scheme}} -\label{Scheme} -\index{Schemes} -\comindex{Scheme} - -The {\tt Scheme} command is a high-level tool for generating -automatically (possibly mutual) induction principles for given types -and sorts. Its syntax follows the schema: -\begin{quote} -{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} \dots\\ - with {\ident$_m$} := Induction for {\ident'$_m$} Sort - {\sort$_m$}} -\end{quote} -where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type -identifiers belonging to the same package of mutual inductive -definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$} -to be mutually recursive definitions. Each term {\ident$_i$} proves a -general principle of mutual induction for objects in type {\term$_i$}. - -\begin{Variants} -\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} \dots\ \\ - with {\ident$_m$} := Minimality for {\ident'$_m$} Sort - {\sort$_m$}} - - Same as before but defines a non-dependent elimination principle more - natural in case of inductively defined relations. - -\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}} - - Tries to generate a boolean equality and a proof of the - decidability of the usual equality. If \ident$_i$ involves - some other inductive types, their equality has to be defined first. - -\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} \dots\\ - with Induction for {\ident$_m$} Sort - {\sort$_m$}} - - If you do not provide the name of the schemes, they will be automatically - computed from the sorts involved (works also with Minimality). - -\end{Variants} -\label{Scheme-examples} - -\firstexample -\example{Induction scheme for \texttt{tree} and \texttt{forest}} - -The definition of principle of mutual induction for {\tt tree} and -{\tt forest} over the sort {\tt Set} is defined by the command: - -\begin{coq_eval} -Reset Initial. -Variables A B : Set. -\end{coq_eval} - -\begin{coq_example*} -Inductive tree : Set := - node : A -> forest -> tree -with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. - -Scheme tree_forest_rec := Induction for tree Sort Set - with forest_tree_rec := Induction for forest Sort Set. -\end{coq_example*} - -You may now look at the type of {\tt tree\_forest\_rec}: - -\begin{coq_example} -Check tree_forest_rec. -\end{coq_example} - -This principle involves two different predicates for {\tt trees} and -{\tt forests}; it also has three premises each one corresponding to a -constructor of one of the inductive definitions. - -The principle {\tt forest\_tree\_rec} shares exactly the same -premises, only the conclusion now refers to the property of forests. - -\begin{coq_example} -Check forest_tree_rec. -\end{coq_example} - -\example{Predicates {\tt odd} and {\tt even} on naturals} - -Let {\tt odd} and {\tt even} be inductively defined as: - -% Reset Initial. -\begin{coq_eval} -Open Scope nat_scope. -\end{coq_eval} - -\begin{coq_example*} -Inductive odd : nat -> Prop := - oddS : forall n:nat, even n -> odd (S n) -with even : nat -> Prop := - | evenO : even 0 - | evenS : forall n:nat, odd n -> even (S n). -\end{coq_example*} - -The following command generates a powerful elimination -principle: - -\begin{coq_example} -Scheme odd_even := Minimality for odd Sort Prop - with even_odd := Minimality for even Sort Prop. -\end{coq_example} - -The type of {\tt odd\_even} for instance will be: - -\begin{coq_example} -Check odd_even. -\end{coq_example} - -The type of {\tt even\_odd} shares the same premises but the -conclusion is {\tt (n:nat)(even n)->(Q n)}. - -\subsection{Automatic declaration of schemes} -\comindex{Set Equality Schemes} -\comindex{Set Elimination Schemes} - -It is possible to deactivate the automatic declaration of the induction - principles when defining a new inductive type with the - {\tt Unset Elimination Schemes} command. It may be -reactivated at any time with {\tt Set Elimination Schemes}. -\\ - -You can also activate the automatic declaration of those boolean equalities -(see the second variant of {\tt Scheme}) with the {\tt Set Equality Schemes} - command. However you have to be careful with this option since -\Coq~ may now reject well-defined inductive types because it cannot compute -a boolean equality for them. - -\subsection{\tt Combined Scheme} -\label{CombinedScheme} -\comindex{Combined Scheme} - -The {\tt Combined Scheme} command is a tool for combining -induction principles generated by the {\tt Scheme} command. -Its syntax follows the schema : -\begin{quote} -{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}} -\end{quote} -where -\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to -the same package of mutual inductive principle definitions. This command -generates {\ident$_0$} to be the conjunction of the principles: it is -built from the common premises of the principles and concluded by the -conjunction of their conclusions. - -\Example -We can define the induction principles for trees and forests using: -\begin{coq_example} -Scheme tree_forest_ind := Induction for tree Sort Prop - with forest_tree_ind := Induction for forest Sort Prop. -\end{coq_example} - -Then we can build the combined induction principle which gives the -conjunction of the conclusions of each individual principle: -\begin{coq_example} -Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind. -\end{coq_example} - -The type of {\tt tree\_forest\_mutrec} will be: -\begin{coq_example} -Check tree_forest_mutind. -\end{coq_example} - -\section{Generation of induction principles with {\tt Functional Scheme}} -\label{FunScheme} -\comindex{Functional Scheme} - -The {\tt Functional Scheme} command is a high-level experimental -tool for generating automatically induction principles -corresponding to (possibly mutually recursive) functions. Its -syntax follows the schema: -\begin{quote} -{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} \dots\ \\ - with {\ident$_m$} := Induction for {\ident'$_m$} Sort - {\sort$_m$}} -\end{quote} -where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function -names (they must be in the same order as when they were defined). -This command generates the induction principles -\ident$_1$\dots\ident$_m$, following the recursive structure and case -analyses of the functions \ident'$_1$ \dots\ \ident'$_m$. - -\Rem -There is a difference between obtaining an induction scheme by using -\texttt{Functional Scheme} on a function defined by \texttt{Function} -or not. Indeed \texttt{Function} generally produces smaller -principles, closer to the definition written by the user. - -\firstexample -\example{Induction scheme for \texttt{div2}} -\label{FunScheme-examples} - -We define the function \texttt{div2} as follows: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example*} -Require Import Arith. -Fixpoint div2 (n:nat) : nat := - match n with - | O => 0 - | S O => 0 - | S (S n') => S (div2 n') - end. -\end{coq_example*} - -The definition of a principle of induction corresponding to the -recursive structure of \texttt{div2} is defined by the command: - -\begin{coq_example} -Functional Scheme div2_ind := Induction for div2 Sort Prop. -\end{coq_example} - -You may now look at the type of {\tt div2\_ind}: - -\begin{coq_example} -Check div2_ind. -\end{coq_example} - -We can now prove the following lemma using this principle: - -\begin{coq_example*} -Lemma div2_le' : forall n:nat, div2 n <= n. -intro n. - pattern n , (div2 n). -\end{coq_example*} - -\begin{coq_example} -apply div2_ind; intros. -\end{coq_example} - -\begin{coq_example*} -auto with arith. -auto with arith. -simpl; auto with arith. -Qed. -\end{coq_example*} - -We can use directly the \texttt{functional induction} -(\ref{FunInduction}) tactic instead of the pattern/apply trick: -\tacindex{functional induction} - -\begin{coq_example*} -Reset div2_le'. -Lemma div2_le : forall n:nat, div2 n <= n. -intro n. -\end{coq_example*} - -\begin{coq_example} -functional induction (div2 n). -\end{coq_example} - -\begin{coq_example*} -auto with arith. -auto with arith. -auto with arith. -Qed. -\end{coq_example*} - -\Rem There is a difference between obtaining an induction scheme for a -function by using \texttt{Function} (see Section~\ref{Function}) and by -using \texttt{Functional Scheme} after a normal definition using -\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for -details. - - -\example{Induction scheme for \texttt{tree\_size}} - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -We define trees by the following mutual inductive type: - -\begin{coq_example*} -Variable A : Set. -Inductive tree : Set := - node : A -> forest -> tree -with forest : Set := - | empty : forest - | cons : tree -> forest -> forest. -\end{coq_example*} - -We define the function \texttt{tree\_size} that computes the size -of a tree or a forest. Note that we use \texttt{Function} which -generally produces better principles. - -\begin{coq_example*} -Function tree_size (t:tree) : nat := - match t with - | node A f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | empty => 0 - | cons t f' => (tree_size t + forest_size f') - end. -\end{coq_example*} - -\Rem \texttt{Function} generates itself non mutual induction -principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}: - -\begin{coq_example} -Check tree_size_ind. -\end{coq_example} - -The definition of mutual induction principles following the recursive -structure of \texttt{tree\_size} and \texttt{forest\_size} is defined -by the command: - -\begin{coq_example*} -Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop -with forest_size_ind2 := Induction for forest_size Sort Prop. -\end{coq_example*} - -You may now look at the type of {\tt tree\_size\_ind2}: - -\begin{coq_example} -Check tree_size_ind2. -\end{coq_example} - -\section{Generation of inversion principles with \tt Derive Inversion} -\label{Derive-Inversion} -\comindex{Derive Inversion} - -The syntax of {\tt Derive Inversion} follows the schema: -\begin{quote} -{\tt Derive Inversion {\ident} with forall - $(\vec{x} : \vec{T})$, $I~\vec{t}$ Sort \sort} -\end{quote} - -This command generates an inversion principle for the -\texttt{inversion \dots\ using} tactic. -\tacindex{inversion \dots\ using} -Let $I$ be an inductive predicate and $\vec{x}$ the variables -occurring in $\vec{t}$. This command generates and stocks the -inversion lemma for the sort \sort~ corresponding to the instance -$\forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf -global} environment. When applied, it is equivalent to having inverted -the instance with the tactic {\tt inversion}. - -\begin{Variants} -\item \texttt{Derive Inversion\_clear {\ident} with forall - $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\ - \comindex{Derive Inversion\_clear} - When applied, it is equivalent to having - inverted the instance with the tactic \texttt{inversion} - replaced by the tactic \texttt{inversion\_clear}. -\item \texttt{Derive Dependent Inversion {\ident} with forall - $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\ - \comindex{Derive Dependent Inversion} - When applied, it is equivalent to having - inverted the instance with the tactic \texttt{dependent inversion}. -\item \texttt{Derive Dependent Inversion\_clear {\ident} with forall - $(\vec{x}:\vec{T})$, $I~\vec{t}$ Sort \sort}\\ - \comindex{Derive Dependent Inversion\_clear} - When applied, it is equivalent to having - inverted the instance with the tactic \texttt{dependent inversion\_clear}. -\end{Variants} - -\Example - -Let us consider the relation \texttt{Le} over natural numbers and the -following variable: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example*} -Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). -Variable P : nat -> nat -> Prop. -\end{coq_example*} - -To generate the inversion lemma for the instance -\texttt{(Le (S n) m)} and the sort \texttt{Prop}, we do: - -\begin{coq_example*} -Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop. -\end{coq_example*} - -\begin{coq_example} -Check leminv. -\end{coq_example} - -Then we can use the proven inversion lemma: - -\begin{coq_eval} -Lemma ex : forall n m:nat, Le (S n) m -> P n m. -intros. -\end{coq_eval} - -\begin{coq_example} -Show. -\end{coq_example} - -\begin{coq_example} -inversion H using leminv. -\end{coq_example} - diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 0ee101c8..833b5c4c 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -400,6 +400,7 @@ through the Require Import command.