Update to latest version of Coq, add MIT licence.

Additive.v

@@ -43,23 +43,23 @@ Proof.
     transitivity r ; assumption.
   - intros q [r [s [H1 [H2 H3]]]].
     exists ((q + r + s) * (1#2)) ; split.
-    + apply (Qle_lt_trans q  ((q+q)*(1#2)) ((q + r + s) * (1 # 2))). 
+    + apply (Qle_lt_trans q  ((q+q)*(1#2)) ((q + r + s) * (1 # 2))).
       ring_simplify; apply Qle_refl.
       apply Qmult_lt_compat_r; [reflexivity | idtac].
        apply (Qplus_lt_r _ _ (-q)); ring_simplify; assumption.
     + exists r, s ; split ; auto.
       setoid_replace (r+s) with ((r+s+r+s)*(1#2)).
       apply Qmult_lt_compat_r. reflexivity.
       destruct (Qplus_lt_l q (r+s) (r+s)) .
-      setoid_replace (q+r+s) with (q+(r+s)); [idtac | ring]. 
+      setoid_replace (q+r+s) with (q+(r+s)); [idtac | ring].
       setoid_replace (r+s+r+s) with (r+s+(r+s)); [auto | ring].
-      ring_simplify; ring. 
+      ring_simplify; ring.
   - intros q r Lqr [r' [s' [H1 [H2 H3]]]].
     exists r', s'; split; auto.
     transitivity q; assumption.
   - intros q [r [s [H1 [H2 H3]]]].
     exists ((q + r + s) * (1#2)) ; split.
-    +apply (Qlt_le_trans ((q + r + s) * (1 # 2)) ((q+q)*(1#2)) q). 
+    +apply (Qlt_le_trans ((q + r + s) * (1 # 2)) ((q+q)*(1#2)) q).
      apply Qmult_lt_compat_r; [reflexivity | idtac].
      destruct (Qplus_lt_r (r+s) q q).
      setoid_replace (q+r+s) with (q+(r+s)); [apply H0;assumption|idtac].
@@ -90,10 +90,10 @@ Proof.
         exists xL, yL; split; auto.
         assert (r-xL-yL<r-q).
           -setoid_replace (r-q) with ((r-q)*(1#2) + (r-q)*(1#2));[idtac|ring].
-           apply (Qlt_trans (r-xL-yL) ((r-q)*(1#2)+yU-yL) ((r-q)*(1#2)+(r-q)*(1#2))).    
+           apply (Qlt_trans (r-xL-yL) ((r-q)*(1#2)+yU-yL) ((r-q)*(1#2)+(r-q)*(1#2))).
            + apply (Qle_lt_trans (r-xL-yL) (xU-xL+yU-yL) ((r-q)*(1#2)+yU-yL)).
              * apply (Qplus_le_r _ _ (xL+yL)%Q) ; ring_simplify ; auto.
-             * apply (Qplus_lt_r _ _ (-yU+yL)%Q) ; ring_simplify. 
+             * apply (Qplus_lt_r _ _ (-yU+yL)%Q) ; ring_simplify.
                setoid_replace ((1 # 2) * r + (-1 # 2) * q) with ((r - q) * (1 # 2)).
                auto. ring_simplify; reflexivity.
            + setoid_replace ((r-q)*(1#2)+yU-yL) with ((r-q)*(1#2)+(yU-yL)).
@@ -102,9 +102,9 @@ Proof.
           -apply (Qplus_lt_l _ _ (r-xL-yL-q)); ring_simplify.
            setoid_replace ((-1#1)*q+r) with (r-q);[auto|apply (Qplus_comm ((-1#1)*q)r)].
         }
-    +left. 
+    +left.
      exists xL, yL; split; auto.
-     apply (Qlt_le_trans q r (xL+yL)); auto. 
+     apply (Qlt_le_trans q r (xL+yL)); auto.
 Defined.
 
 (** Opposite value. *)
@@ -122,17 +122,15 @@ Proof.
     rewrite (Qopp_involutive q); assumption.
   - intros q r H G.
     apply (upper_upper _ (- r) _); [idtac | assumption].
-    apply Qopp_lt_compat.
-    rewrite 2 Qopp_involutive; assumption.
+    now apply Qopp_lt_compat.
   - intros q H.
     destruct (upper_open x (-q)) as [s [G1 G2]]; [assumption | idtac].
     exists (-s); split.
     apply Qopp_lt_shift_r; assumption.
     rewrite Qopp_involutive; assumption.
   - intros q r H G.
     apply (lower_lower _ _ (- q)) ; [idtac | assumption].
-    apply Qopp_lt_compat.
-    rewrite 2 Qopp_involutive; assumption.
+    now apply Qopp_lt_compat.
   - intros q H.
     destruct (lower_open x (-q)) as [s [G1 G2]]; [assumption | idtac].
     exists (-s); split.
@@ -143,7 +141,7 @@ Proof.
     tauto.
   - intros q r H.
     destruct (located x (-r) (-q)).
-    + apply Qopp_lt_compat; rewrite 2 Qopp_involutive; assumption.
+    + now apply Qopp_lt_compat.
     + right; assumption.
     + left; assumption.
 Defined.
@@ -213,14 +211,14 @@ Proof.
       apply Qplus_lt_l.
       assumption.
     + split ; auto.
-      destruct (lower_open z r) as [t [H1 H2]]. assumption. 
+      destruct (lower_open z r) as [t [H1 H2]]. assumption.
       exists r', t; split; auto.
       rewrite (Qplus_comm r r').
       apply Qplus_lt_r; auto.
   - intros q [x' [yz' [H [Hx [y' [z' [H1 [Hy Hz]]]]]]]].
     exists (x' + y')%Q, z' ; split.
     + transitivity (x' + yz')%Q ; auto.
-      apply (Qplus_lt_r _ _ (-x')); ring_simplify; assumption. 
+      apply (Qplus_lt_r _ _ (-x')); ring_simplify; assumption.
     + split ; auto.
       destruct (lower_open x x') as [t [G1 G2]] ; auto.
       exists t, y'; split; auto.
@@ -279,7 +277,7 @@ Proof.
      apply (lower_below_upper x); [assumption|auto].
   - assert (G : (-q > 0)%Q).
     + apply (Qplus_lt_r _ _ q) ; ring_simplify ; auto.
-    + destruct (archimedean x _ G) as [a [b [A [B C]]]]. 
+    + destruct (archimedean x _ G) as [a [b [A [B C]]]].
       exists a, (-b)%Q; repeat split; auto.
       apply (Qplus_lt_r _ _ (b-a-q)%Q) ; ring_simplify ; auto.
       cut (upper x (--b)) ; auto.
@@ -300,7 +298,7 @@ Proof.
     setoid_replace (-1*q) with (-q)%Q. apply H. ring.
     apply (upper_proper r1 r). ring. apply H.
     apply (upper_proper r2 s). ring. apply H.
-  - intros q [r [s H]]. exists (-r)%Q,(-s)%Q. 
+  - intros q [r [s H]]. exists (-r)%Q,(-s)%Q.
     repeat split. rewrite <- (Qplus_lt_l _ _ (r+s+q)). ring_simplify.
     apply H. apply H. apply H.
 Qed.

Archimedean.v

@@ -59,7 +59,7 @@ Proof.
   - intro n. apply located. apply Qplus_lt_r. apply Qmult_lt_r.
     apply Qinv_lt_0_compat. unfold Qlt. simpl. unfold Z.lt. auto.
     apply Qmult_lt_r. assumption. rewrite <- Zlt_Qlt.
-    apply inj_lt. apply le_refl.
+    apply inj_lt. apply Nat.le_refl.
   - simpl. rewrite Qmult_0_l. unfold Qdiv. rewrite Qmult_0_l.
     rewrite Qplus_0_r. assumption.
   - apply (uu r). exact u. rewrite <- Qplus_0_l. rewrite <- (Qplus_opp_r q).

Cauchy.v

@@ -33,7 +33,7 @@ Proof.
   apply Qabs_triangle. rewrite Qabs_opp. apply Qplus_lt_le_compat.
   - apply H. apply H0.
   - apply Qlt_le_weak. apply H. apply H1.
-Qed. 
+Qed.
 
 Definition CauchyQ_lower (un : nat -> Q) (q : Q) : Prop
   := exists (r:Q) (n:nat), Qlt 0 r /\ forall i:nat, le n i -> Qlt (q+r) (un i).
@@ -46,14 +46,14 @@ Lemma CauchyQ_lower_open
 Proof.
   intros. destruct H as [r [n H]].
   exists (q+r/2). split.
-  rewrite <- Qplus_0_r, <- Qplus_assoc, Qplus_lt_r, Qplus_0_l. 
+  rewrite <- Qplus_0_r, <- Qplus_assoc, Qplus_lt_r, Qplus_0_l.
   rewrite <- (Qmult_0_l (/2)). apply Qmult_lt_r.
   reflexivity. apply H.
-  exists (r/2), n. split. 
+  exists (r/2), n. split.
   rewrite <- (Qmult_0_l (/2)). apply Qmult_lt_r.
   reflexivity. apply H.
   intros. rewrite <- Qplus_assoc.
-  setoid_replace (r/2+r/2) with r. apply H. exact H0. field. 
+  setoid_replace (r/2+r/2) with r. apply H. exact H0. field.
 Qed.
 
 Lemma CauchyQ_upper_open
@@ -65,11 +65,11 @@ Proof.
   rewrite <- (Qplus_0_r q), <- Qplus_assoc, <- (Qplus_lt_r _ _ (-q+r/2)).
   ring_simplify. rewrite <- (Qmult_0_l (/2)). apply Qmult_lt_r.
   reflexivity. apply H.
-  exists (r/2), n. split. 
+  exists (r/2), n. split.
   rewrite <- (Qmult_0_l (/2)). apply Qmult_lt_r.
   reflexivity. apply H.
   intros. unfold Qminus. rewrite <- Qplus_assoc.
-  setoid_replace (-(r/2)+ -(r/2)) with (-r)%Q. apply H. exact H0. field. 
+  setoid_replace (-(r/2)+ -(r/2)) with (-r)%Q. apply H. exact H0. field.
 Qed.
 
 Lemma CauchyQ_located :
@@ -79,30 +79,30 @@ Proof.
   intros un q r cau H. assert (Qlt 0 ((r-q)/4)).
   { unfold Qdiv. rewrite <- (Qmult_0_l (/4)).
     apply Qmult_lt_r. reflexivity.
-    unfold Qminus. rewrite <- Qlt_minus_iff. exact H. } 
+    unfold Qminus. rewrite <- Qlt_minus_iff. exact H. }
   destruct (cau ((r-q)/4) H0) as [n nmaj].
   destruct (Qlt_le_dec (un n) ((q+r)/2)).
   - right. exists ((r-q)/4), n. split. exact H0. intros.
-    specialize (nmaj n i (le_refl _) H1).
+    specialize (nmaj n i (Nat.le_refl _) H1).
     rewrite <- (Qplus_lt_r _ _ (un n + - un i)). ring_simplify.
     apply (Qlt_le_trans _ ((q+r)/2) _ q0).
     rewrite <- (Qplus_le_r _ _ ((r-q)/4+-r)). ring_simplify.
     setoid_replace (un n + -1 * un i) with (un n - un i). 2: ring.
     apply Qlt_le_weak, Qabs_Qle_condition in nmaj.
     apply (Qle_trans _ (-((r-q)/4))). 2: apply nmaj.
-    apply Qle_minus_iff. 
+    apply Qle_minus_iff.
     setoid_replace (- ((r - q) / 4) + - ((r - q) / 4 + -1 * r + (q + r) / 2))
       with 0.
     2: field. apply Qle_refl.
   - left. exists ((r-q)/4), n. split. exact H0. intros.
-    specialize (nmaj n i (le_refl _) H1).
+    specialize (nmaj n i (Nat.le_refl _) H1).
     rewrite <- (Qplus_lt_r _ _ (un n + - un i)). ring_simplify.
     apply (Qlt_le_trans _ ((q+r)/2)). 2: exact q0. clear q0.
     rewrite <- (Qplus_lt_r _ _ (-q-(r-q)/4)). ring_simplify.
     setoid_replace (un n + -1 * un i) with (un n - un i). 2: ring.
     apply (Qle_lt_trans _ (Qabs (un n - un i))). apply Qle_Qabs.
     apply (Qlt_le_trans _ ((r-q)/4) _ nmaj).
-    apply Qle_minus_iff. 
+    apply Qle_minus_iff.
     setoid_replace (-1 * q + -1 * ((r - q) / 4) + (q + r) / 2 + - ((r - q) / 4))
       with 0.
     2: field. apply Qle_refl.
@@ -121,14 +121,14 @@ Proof.
     exists r, n. split. apply H0. intros. rewrite H. apply H0. exact H1.
   - destruct (cau 1) as [n nmaj]. reflexivity.
     exists (un n - 2), 1, n.
-    split. reflexivity. intros. specialize (nmaj n i (le_refl _) H).
+    split. reflexivity. intros. specialize (nmaj n i (Nat.le_refl _) H).
     rewrite <- (Qplus_lt_l _ _ (1-un i)). ring_simplify.
     apply (Qle_lt_trans _ (Qabs (un n - un i))). 2: exact nmaj.
     setoid_replace (un n + -1 * un i) with (un n - un i). 2: ring.
     apply Qle_Qabs.
   - destruct (cau 1) as [n nmaj]. reflexivity.
     exists (un n + 2), 1, n.
-    split. reflexivity. intros. specialize (nmaj n i (le_refl _) H).
+    split. reflexivity. intros. specialize (nmaj n i (Nat.le_refl _) H).
     rewrite Qabs_Qminus in nmaj.
     rewrite <- (Qplus_lt_l _ _ (-un n)). ring_simplify.
     apply (Qle_lt_trans _ (Qabs (un i - un n))). 2: exact nmaj.
@@ -141,7 +141,7 @@ Proof.
   - intros. destruct H0 as [s [n [H0 H1]]].
     exists s, n. split. exact H0. intros.
     apply (Qlt_trans _ (q-s) _ (H1 i H2)).
-    unfold Qminus. rewrite Qplus_lt_l. exact H. 
+    unfold Qminus. rewrite Qplus_lt_l. exact H.
   - apply CauchyQ_upper_open.
   - intros q [[r [n H]] [s [m H0]]]. destruct H, H0.
     specialize (H1 (max n m) (Nat.le_max_l _ _)).
@@ -209,8 +209,8 @@ Lemma pos_sum_more : forall (u : nat -> Q)
     -> le n p -> Qle (sum_f_Q0 u n) (sum_f_Q0 u p).
 Proof.
   intros. destruct (Nat.le_exists_sub n p H0). destruct H1. subst p.
-  rewrite plus_comm.
-  destruct x. rewrite plus_0_r. apply Qle_refl. rewrite Nat.add_succ_r.
+  rewrite Nat.add_comm.
+  destruct x. rewrite Nat.add_0_r. apply Qle_refl. rewrite Nat.add_succ_r.
   replace (S (n + x)) with (S n + x)%nat. rewrite <- Qplus_0_r.
   rewrite sum_assoc. rewrite Qplus_le_r.
   apply cond_pos_sum. intros. apply H. auto.
@@ -267,11 +267,11 @@ Proof.
     2: ring. ring_simplify. rewrite Qplus_0_l.
     apply (Qle_trans _ (sum_f_Q0 (fun k0 : nat => Qabs (un (S n + k0)%nat)) k)).
     apply multiTriangleIneg. apply sum_Qle. intros.
-    apply H. simpl. rewrite plus_comm. reflexivity.
-    assumption. assumption.  
+    apply H. simpl. rewrite Nat.add_comm. reflexivity.
+    assumption. assumption.
   - destruct (Nat.le_exists_sub p n) as [k [maj _]]. unfold lt in l.
-    apply (le_trans p (S p)). apply le_S. apply le_refl. assumption.
-    subst n. rewrite max_l. rewrite min_r. 
+    apply (Nat.le_trans p (S p)). apply le_S. apply Nat.le_refl. assumption.
+    subst n. rewrite max_l. rewrite min_r.
     destruct k. simpl plus. unfold Qminus. rewrite Qplus_opp_r.
     rewrite Qplus_opp_r. rewrite Qabs_pos. apply Qle_refl. apply Qle_refl.
     replace (S k + p)%nat with (S p + k)%nat.
@@ -281,9 +281,9 @@ Proof.
     2: ring.
     apply (Qle_trans _ (sum_f_Q0 (fun k0 : nat => Qabs (un (S p + k0)%nat)) k)).
     apply multiTriangleIneg. apply sum_Qle. intros.
-    apply H. simpl. rewrite plus_comm. reflexivity.
-    apply (le_trans p (S p)). apply le_S. apply le_refl. assumption.
-    apply (le_trans p (S p)). apply le_S. apply le_refl. assumption.
+    apply H. simpl. rewrite Nat.add_comm. reflexivity.
+    apply (Nat.le_trans p (S p)). apply le_S. apply Nat.le_refl. assumption.
+    apply (Nat.le_trans p (S p)). apply le_S. apply Nat.le_refl. assumption.
 Qed.
 
 (* The constructive analog of the least upper bound principle. *)
@@ -298,13 +298,13 @@ Proof.
   apply Abs_sum_maj. apply H.
   setoid_replace (sum_f_Q0 vn (max i j) - sum_f_Q0 vn (min i j))%Q
     with (Qabs (sum_f_Q0 vn (max i j) - (sum_f_Q0 vn (min i j)))).
-  apply nmaj. apply (le_trans _ i). assumption. apply Nat.le_max_l.
-  apply Nat.min_case. apply (le_trans _ i). assumption. apply le_refl.
+  apply nmaj. apply (Nat.le_trans _ i). assumption. apply Nat.le_max_l.
+  apply Nat.min_case. apply (Nat.le_trans _ i). assumption. apply Nat.le_refl.
   exact H2. rewrite Qabs_pos. reflexivity.
   apply (Qplus_le_l _ _ (sum_f_Q0 vn (Init.Nat.min i j))).
   ring_simplify. apply pos_sum_more.
   intros. apply (Qle_trans _ (Qabs (un k))). apply Qabs_nonneg.
-  apply H. apply (le_trans _ i). apply Nat.le_min_l. apply Nat.le_max_l.
+  apply H. apply (Nat.le_trans _ i). apply Nat.le_min_l. apply Nat.le_max_l.
 Qed.
 
 Lemma GeoHalfSum : forall k:nat,

DecOrder.v

@@ -1,7 +1,7 @@
 (** When doing classical analysis, discontinuous real functions are often
     defined by testing a comparison, like
     f x := if 0 < x then 1 else 0.
-    
+
     This requires the following disjunction in sort Type,
     { x < y } + { ~(x < y) }.
 
@@ -53,7 +53,7 @@ Qed.
 
 Lemma DecOrderImpliesLPO : (forall x:R, { 0 < x } + { ~(0 < x) }) -> LPO.
 Proof.
-  intros decOrder un. 
+  intros decOrder un.
   pose (fun n:nat => if un n then (/2)^(Z.of_nat n) else 0%Q) as vn.
   assert (CauchyQ (sum_f_Q0 vn)).
   { apply (Cauchy_series_maj _ (fun n:nat => (/2)^(Z.of_nat n))).
@@ -64,14 +64,14 @@ Proof.
   destruct (decOrder (CauchyQ_R (sum_f_Q0 vn) H)) as [H0|H0].
   - left. destruct H0 as [q [qPos H0]].
     destruct H0 as [r [n [rPos H0]]].
-    specialize (H0 n (le_refl _)). simpl in qPos.
+    specialize (H0 n (Nat.le_refl _)). simpl in qPos.
     apply (Qlt_trans 0 (q+r)) in H0. apply Find_positive_in_sum in H0.
     destruct H0. exists x. unfold vn in H0.
     destruct (un x) eqn:des. reflexivity.
     exfalso. exact (Qlt_irrefl 0 H0).
     intros. unfold vn. destruct (un k). apply Qpower_pos. discriminate.
     discriminate. rewrite <- Qplus_0_r. apply Qplus_lt_le_compat.
-    exact qPos. apply Qlt_le_weak. exact rPos. 
+    exact qPos. apply Qlt_le_weak. exact rPos.
   - right. intro n. apply Rnot_lt_le in H0.
     unfold Rle, CauchyQ_R in H0; simpl in H0.
     destruct (un n) eqn:des. 2: reflexivity. exfalso.
@@ -91,7 +91,7 @@ Proof.
     rewrite Qmult_inv_r. field_simplify. reflexivity.
     apply Qpower_nonzero. intro abs. discriminate.
     apply Qpower_nonzero. intro abs. discriminate.
-    apply Qpower_strictly_pos. reflexivity. 
+    apply Qpower_strictly_pos. reflexivity.
     rewrite Qpower_plus. simpl. rewrite Qinv_mult_distr. reflexivity.
     intro abs. discriminate.
     apply (Qle_trans _ (vn n)).

LICENSE

@@ -0,0 +1,18 @@
+Copyright © 2024 Andrej Bauer, Vincent Semeria
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the “Software”), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+the Software, and to permit persons to whom the Software is furnished to do so,
+subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

MiscLemmas.v

@@ -1,6 +1,9 @@
 (** Various lemmas that seem to be missing from the standard library. *)
 
 Require Import QArith Qminmax Qabs Lia.
+Require Import Qpower.
+
+Section MiscLemmas.
 
 Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x => g (f x).
 Hint Unfold compose : core.
@@ -187,8 +190,6 @@ Proof.
     apply Qplus_le_l; assumption.
 Qed.
 
-Require Import Qpower.
-
 Lemma Qpower_zero: forall p, ~p == 0 -> p^0 == 1.
 Proof.
 intros p H.
@@ -304,3 +305,5 @@ Proof.
     + assumption.
     + apply (Qle_trans _ q) ; assumption.
 Qed.
+
+End MiscLemmas.