aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Logic/Hurkens.v2
-rw-r--r--theories/MSets/MSetEqProperties.v4
-rw-r--r--theories/QArith/Qreals.v4
-rw-r--r--theories/Reals/ArithProp.v4
-rw-r--r--theories/Reals/RIneq.v17
-rw-r--r--theories/Reals/R_Ifp.v21
-rw-r--r--theories/Reals/R_sqr.v2
-rw-r--r--theories/Reals/Rbasic_fun.v2
-rw-r--r--theories/Reals/Rfunctions.v17
-rw-r--r--theories/Reals/SplitRmult.v2
10 files changed, 41 insertions, 34 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 9aed952183..d9e89d6b91 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -72,7 +72,7 @@
- [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type
Theory", 2001, revised 2007
- (see {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
+ (see external link {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
*)
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 303acf7ae2..e3ff4979a9 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -18,6 +18,8 @@
[equal s s'=true] instead of [Equal s s'], etc. *)
Require Import MSetProperties Zerob Sumbool Lia DecidableTypeEx.
+Require FSetEqProperties.
+
Module WEqPropertiesOn (Import E:DecidableType)(M:WSetsOn E).
Module Import MP := WPropertiesOn E M.
@@ -857,7 +859,7 @@ intros.
rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros. do 3 (rewrite fold_add; auto with fset). lia.
+intros. do 3 (rewrite fold_add by auto with fset). lia.
do 3 rewrite fold_empty;auto.
Qed.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 5b3d6ea30e..b1f0d9bc39 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-Require Export Rbase.
+Require Import Rdefinitions Raxioms RIneq.
Require Export QArith_base.
(** Injection of rational numbers into real numbers. *)
@@ -48,7 +48,7 @@ set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
set (Y2 := IZR (Zpos y2)) in *.
assert ((X1 * Y2)%R = (Y1 * X2)%R).
unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.
- apply IZR_eq; auto.
+f_equal; auto.
clear H.
field_simplify_eq; auto.
rewrite H0; ring.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index cbf90c5adb..0cad621692 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
Require Import Rbasic_fun.
Require Import Even.
Require Import Div2.
@@ -85,7 +85,7 @@ Proof.
assert (H1 := le_INR _ _ H).
do 2 rewrite mult_INR in H1.
apply Rmult_le_reg_l with (INR 2).
- replace (INR 2) with 2; [ prove_sup0 | reflexivity ].
+ apply lt_0_INR. apply Nat.lt_0_2.
assumption.
Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 229e6018ca..b0d7b26a86 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -19,7 +19,7 @@ Require Export Raxioms.
Require Import Rpow_def.
Require Import Zpower.
Require Export ZArithRing.
-Require Import Lia.
+Require Import Ztac.
Require Export RealField.
Local Open Scope Z_scope.
@@ -1875,7 +1875,7 @@ Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m.
Proof.
intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H);
rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
- intro; lia.
+ apply Zminus_eq.
Qed.
(**********)
@@ -1913,21 +1913,24 @@ Qed.
Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
Proof.
intros m n H; apply Rnot_lt_ge; red; intro.
- generalize (lt_IZR m n H0); intro; lia.
+ generalize (lt_IZR m n H0); intro.
+ slia H H1.
Qed.
Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
Proof.
intros m n H; apply Rnot_gt_le; red; intro.
- unfold Rgt in H0; generalize (lt_IZR n m H0); intro; lia.
+ unfold Rgt in H0; generalize (lt_IZR n m H0); intro.
+ slia H H1.
Qed.
Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
Proof.
intros m n H; cut (m <= n)%Z.
intro H0; elim (IZR_le m n H0); intro; auto.
- generalize (eq_IZR m n H1); intro; exfalso; lia.
- lia.
+ generalize (eq_IZR m n H1); intro; exfalso.
+ slia H H3.
+ normZ. slia H H0.
Qed.
Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
@@ -1954,7 +1957,7 @@ Lemma one_IZR_r_R1 :
forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
Proof.
intros r z x [H1 H2] [H3 H4].
- cut ((z - x)%Z = 0%Z). lia.
+ apply Zminus_eq.
apply one_IZR_lt1.
rewrite <- Z_R_minus; split.
replace (-1) with (r - (r + 1)).
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 5f0747d869..d9820f9444 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -13,8 +13,8 @@
(* *)
(**********************************************************)
-Require Import Rbase.
-Require Import Lia.
+Require Import Rdefinitions Raxioms RIneq.
+Require Import Ztac.
Local Open Scope R_scope.
(*********************************************************)
@@ -60,7 +60,7 @@ Proof.
apply lt_IZR in H1.
rewrite <- minus_IZR in H2.
apply le_IZR in H2.
- lia.
+ normZ. slia H2 HZ. slia H1 HZ.
Qed.
(**********)
@@ -229,8 +229,8 @@ Proof.
rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H.
rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H;
generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H);
- intros; clear H H0; unfold Int_part at 1;
- lia.
+ intros; clear H H0; unfold Int_part at 1.
+ normZ. slia H HZ. slia H0 HZ.
Qed.
(**********)
@@ -322,8 +322,8 @@ Proof.
generalize (Rlt_le (IZR (Int_part r1 - Int_part r2 - 1)) (r1 - r2) H);
intro; clear H;
generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0);
- intros; clear H0 H1; unfold Int_part at 1;
- lia.
+ intros; clear H0 H1; unfold Int_part at 1.
+ normZ. slia H HZ. slia H0 HZ.
Qed.
(**********)
@@ -437,7 +437,8 @@ Proof.
rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0;
rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0;
generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0);
- intro; clear H H0; unfold Int_part at 1; lia.
+ intro; clear H H0; unfold Int_part at 1.
+ normZ. slia H HZ. slia H0 HZ.
Qed.
(**********)
@@ -498,8 +499,8 @@ Proof.
rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1;
rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1;
generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1);
- intro; clear H0 H1; unfold Int_part at 1;
- lia.
+ intro; clear H0 H1; unfold Int_part at 1.
+ normZ. slia H HZ. slia H0 HZ.
Qed.
(**********)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 1a74582b71..e6c6e8bf48 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
Require Import Rbasic_fun.
Local Open Scope R_scope.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index efca826077..7e59639dd4 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -13,7 +13,7 @@
(* *)
(*********************************************************)
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
Require Import R_Ifp.
Local Open Scope R_scope.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 7f9e019c5b..a63df38808 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -17,7 +17,7 @@
(********************************************************)
Require Export ArithRing.
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
Require Export Rpow_def.
Require Export R_Ifp.
Require Export Rbasic_fun.
@@ -25,8 +25,8 @@ Require Export R_sqr.
Require Export SplitAbsolu.
Require Export SplitRmult.
Require Export ArithProp.
-Require Import Lia.
Require Import Zpower.
+Require Import Ztac.
Local Open Scope nat_scope.
Local Open Scope R_scope.
@@ -122,7 +122,7 @@ Hint Resolve pow_lt: real.
Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
Proof.
intros x n; elim n; simpl; auto with real.
- intros H' H'0; exfalso; lia.
+ intros H' H'0; exfalso. apply (Nat.lt_irrefl 0); assumption.
intros n0; case n0.
simpl; rewrite Rmult_1_r; auto.
intros n1 H' H'0 H'1.
@@ -262,14 +262,14 @@ Proof.
elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0;
apply
(Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
- rewrite INR_IZR_INZ; apply IZR_ge; lia.
+ rewrite INR_IZR_INZ; apply IZR_ge. normZ. slia H3 H5.
unfold Rge; left; assumption.
exists 0%nat;
apply
(Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
- rewrite INR_IZR_INZ; apply IZR_ge; simpl; lia.
+ rewrite INR_IZR_INZ; apply IZR_ge; simpl. normZ. slia H2 H3.
unfold Rge; left; assumption.
- lia.
+ apply Z.le_ge_cases.
Qed.
Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.
@@ -745,7 +745,8 @@ Proof.
- now simpl; rewrite Rmult_1_l.
- now rewrite <- !pow_powerRZ, Rpow_mult_distr.
- destruct Hmxy as [H|H].
- + assert(m = 0) as -> by now lia.
+ + assert(m = 0) as -> by
+ (destruct n; [assumption| subst; simpl in H; lia_contr]).
now rewrite <- Hm, Rmult_1_l.
+ assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l.
assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r.
@@ -808,7 +809,7 @@ Proof.
ring.
rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n).
intro H; rewrite H; simpl; ring.
- lia.
+ apply Nat.add_1_r.
Qed.
Lemma sum_f_R0_triangle :
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v
index be2b5a73f3..cad1525580 100644
--- a/theories/Reals/SplitRmult.v
+++ b/theories/Reals/SplitRmult.v
@@ -11,7 +11,7 @@
(*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*)
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
Ltac split_Rmult :=
match goal with
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:30:18 +0000