aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Compat/Coq87.v1
-rw-r--r--theories/Compat/Coq88.v11
-rw-r--r--theories/Init/Notations.v1
-rw-r--r--theories/Init/Peano.v4
-rw-r--r--theories/Init/Specif.v1
-rw-r--r--theories/Logic/ChoiceFacts.v4
-rw-r--r--theories/QArith/QArith_base.v46
-rw-r--r--theories/QArith/Qabs.v8
-rw-r--r--theories/QArith/Qcanon.v4
-rw-r--r--theories/QArith/Qpower.v4
-rw-r--r--theories/QArith/Qreals.v4
-rw-r--r--theories/QArith/Qreduction.v14
-rw-r--r--theories/QArith/Qround.v12
-rw-r--r--theories/Reals/Ranalysis5.v62
-rw-r--r--theories/Sets/Multiset.v4
-rw-r--r--theories/Sets/Uniset.v4
-rw-r--r--theories/Sorting/Heap.v2
17 files changed, 92 insertions, 94 deletions
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
index 89556ee75..dc1397aff 100644
--- a/theories/Compat/Coq87.v
+++ b/theories/Compat/Coq87.v
@@ -9,6 +9,7 @@
(************************************************************************)
(** Compatibility file for making Coq act similar to Coq v8.7 *)
+Require Export Coq.Compat.Coq88.
(* In 8.7, omega wasn't taking advantage of local abbreviations,
see bug 148 and PR#768. For adjusting this flag, we're forced to
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
new file mode 100644
index 000000000..4142af05d
--- /dev/null
+++ b/theories/Compat/Coq88.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.8 *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 683a442cb..72073bb4f 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -77,6 +77,7 @@ Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x & P }" (at level 0, x at level 99).
Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 73c8c5ef4..d5322d094 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -92,7 +92,9 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
induction n; simpl; auto.
Qed.
-Hint Resolve plus_n_O: core.
+
+Remove Hints eq_refl : core.
+Hint Resolve plus_n_O eq_refl: core. (* We want eq_refl to have higher priority than plus_n_O *)
Lemma plus_O_n : forall n:nat, 0 + n = n.
Proof.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 137bd3a0f..b6afba29a 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -51,6 +51,7 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
+Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
type_scope.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 9fd52866e..238ac7df0 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -28,6 +28,8 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
[[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997.
*)
+Require Import RelationClasses Logic.
+
Set Implicit Arguments.
Local Unset Intuition Negation Unfolding.
@@ -125,8 +127,6 @@ Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) :=
formulation of choice); Note also a typo in its intended
formulation in [[Werner97]]. *)
-Require Import RelationClasses Logic.
-
Definition RepresentativeFunctionalChoice_on :=
forall R:A->A->Prop,
(Equivalence R) ->
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 467f263be..35706e7fa 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -227,9 +227,7 @@ Infix "/" := Qdiv : Q_scope.
(** A light notation for [Zpos] *)
-Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope.
-
-Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z ('b).
+Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b).
Proof.
unfold Qeq. simpl. ring.
Qed.
@@ -242,9 +240,9 @@ Proof.
Open Scope Z_scope.
intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
simpl_mult; ring_simplify.
- replace (p1 * 'r2 * 'q2) with (p1 * 'q2 * 'r2) by ring.
+ replace (p1 * Zpos r2 * Zpos q2) with (p1 * Zpos q2 * Zpos r2) by ring.
rewrite H.
- replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring.
+ replace (r1 * Zpos p2 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * Zpos p2 * Zpos q2) by ring.
rewrite H0.
ring.
Close Scope Z_scope.
@@ -255,7 +253,7 @@ Proof.
unfold Qeq, Qopp; simpl.
Open Scope Z_scope.
intros x y H; simpl.
- replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring.
+ replace (- Qnum x * Zpos (Qden y)) with (- (Qnum x * Zpos (Qden y))) by ring.
rewrite H; ring.
Close Scope Z_scope.
Qed.
@@ -272,9 +270,9 @@ Proof.
Open Scope Z_scope.
intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
intros; simpl_mult; ring_simplify.
- replace (q1 * s1 * 'p2) with (q1 * 'p2 * s1) by ring.
+ replace (q1 * s1 * Zpos p2) with (q1 * Zpos p2 * s1) by ring.
rewrite <- H.
- replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring.
+ replace (p1 * r1 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * p1 * Zpos q2) by ring.
rewrite H0.
ring.
Close Scope Z_scope.
@@ -305,13 +303,13 @@ Proof.
unfold Qeq, Qcompare.
Open Scope Z_scope.
intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *.
- rewrite <- (Zcompare_mult_compat (q2*s2) (p1*'r2)).
- rewrite <- (Zcompare_mult_compat (p2*r2) (q1*'s2)).
- change ('(q2*s2)) with ('q2 * 's2).
- change ('(p2*r2)) with ('p2 * 'r2).
- replace ('q2 * 's2 * (p1*'r2)) with ((p1*'q2)*'r2*'s2) by ring.
+ rewrite <- (Zcompare_mult_compat (q2*s2) (p1*Zpos r2)).
+ rewrite <- (Zcompare_mult_compat (p2*r2) (q1*Zpos s2)).
+ change (Zpos (q2*s2)) with (Zpos q2 * Zpos s2).
+ change (Zpos (p2*r2)) with (Zpos p2 * Zpos r2).
+ replace (Zpos q2 * Zpos s2 * (p1*Zpos r2)) with ((p1*Zpos q2)*Zpos r2*Zpos s2) by ring.
rewrite H.
- replace ('q2 * 's2 * (r1*'p2)) with ((r1*'s2)*'q2*'p2) by ring.
+ replace (Zpos q2 * Zpos s2 * (r1*Zpos p2)) with ((r1*Zpos s2)*Zpos q2*Zpos p2) by ring.
rewrite H'.
f_equal; ring.
Close Scope Z_scope.
@@ -572,8 +570,8 @@ Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.
Proof.
unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
Open Scope Z_scope.
- apply Z.mul_le_mono_pos_r with ('y2); [easy|].
- apply Z.le_trans with (y1 * 'x2 * 'z2).
+ apply Z.mul_le_mono_pos_r with (Zpos y2); [easy|].
+ apply Z.le_trans with (y1 * Zpos x2 * Zpos z2).
- rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
- rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
now apply Z.mul_le_mono_pos_r.
@@ -620,8 +618,8 @@ Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
Proof.
unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
Open Scope Z_scope.
- apply Z.mul_lt_mono_pos_r with ('y2); [easy|].
- apply Z.le_lt_trans with (y1 * 'x2 * 'z2).
+ apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].
+ apply Z.le_lt_trans with (y1 * Zpos x2 * Zpos z2).
- rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
- rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
now apply Z.mul_lt_mono_pos_r.
@@ -632,8 +630,8 @@ Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z.
Proof.
unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros.
Open Scope Z_scope.
- apply Z.mul_lt_mono_pos_r with ('y2); [easy|].
- apply Z.lt_le_trans with (y1 * 'x2 * 'z2).
+ apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].
+ apply Z.lt_le_trans with (y1 * Zpos x2 * Zpos z2).
- rewrite Z.mul_shuffle0. now apply Z.mul_lt_mono_pos_r.
- rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
now apply Z.mul_le_mono_pos_r.
@@ -723,9 +721,9 @@ Proof.
match goal with |- ?a <= ?b => ring_simplify a b end.
rewrite Z.add_comm.
apply Z.add_le_mono.
- match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+ match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.
auto with zarith.
- match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+ match goal with |- ?a <= ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.
auto with zarith.
Close Scope Z_scope.
Qed.
@@ -740,9 +738,9 @@ Proof.
match goal with |- ?a < ?b => ring_simplify a b end.
rewrite Z.add_comm.
apply Z.add_le_lt_mono.
- match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+ match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.
auto with zarith.
- match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+ match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.
do 2 (apply Z.mul_lt_mono_pos_r;try easy).
Close Scope Z_scope.
Qed.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 48be89417..31eb41bc9 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -28,8 +28,8 @@ intros [xn xd] [yn yd] H.
simpl.
unfold Qeq in *.
simpl in *.
-change (' yd)%Z with (Z.abs (' yd)).
-change (' xd)%Z with (Z.abs (' xd)).
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
repeat rewrite <- Z.abs_mul.
congruence.
Qed.
@@ -88,8 +88,8 @@ unfold Qplus.
unfold Qle.
simpl.
apply Z.mul_le_mono_nonneg_r;auto with *.
-change (' yd)%Z with (Z.abs (' yd)).
-change (' xd)%Z with (Z.abs (' xd)).
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
repeat rewrite <- Z.abs_mul.
apply Z.abs_triangle.
Qed.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index e25f69c31..1510a7b82 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -30,7 +30,7 @@ Lemma Qred_identity :
Proof.
intros (a,b) H; simpl in *.
rewrite <- Z.ggcd_gcd in H.
- generalize (Z.ggcd_correct_divisors a ('b)).
+ generalize (Z.ggcd_correct_divisors a (Zpos b)).
destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst.
rewrite !Z.mul_1_l. now intros (<-,<-).
Qed.
@@ -39,7 +39,7 @@ Lemma Qred_identity2 :
forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.
Proof.
intros (a,b) H; simpl in *.
- generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+ generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
rewrite <- Z.ggcd_gcd.
destruct Z.ggcd as (g,(aa,bb)); simpl in *.
injection H as <- <-. intros H (_,H').
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 3fd78f092..010782209 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -90,7 +90,7 @@ rewrite Qinv_power.
reflexivity.
Qed.
-Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n.
+Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z (Zpos p))^n.
Proof.
intros n p.
rewrite Qmake_Qdiv.
@@ -190,7 +190,7 @@ unfold Z.succ.
rewrite Zpower_exp; auto with *; try discriminate.
rewrite Qpower_plus' by discriminate.
rewrite <- IHn by discriminate.
-replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring.
+replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring.
ring_simplify.
reflexivity.
Qed.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 14ab1700e..c83296259 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -167,8 +167,8 @@ unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden.
simpl; intros; elim H; trivial.
intros; field; auto.
intros;
- change (IZR (Zneg x2)) with (- IZR (' x2))%R;
- change (IZR (Zneg p)) with (- IZR (' p))%R;
+ change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R;
+ change (IZR (Zneg p)) with (- IZR (Zpos p))%R;
simpl; field; (*auto 8 with real.*)
repeat split; auto; auto with real.
Qed.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 7b08515d2..17307c827 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -21,14 +21,14 @@ Notation Z2P_correct := Z2Pos.id (only parsing).
Definition Qred (q:Q) :=
let (q1,q2) := q in
- let (r1,r2) := snd (Z.ggcd q1 ('q2))
+ let (r1,r2) := snd (Z.ggcd q1 (Zpos q2))
in r1#(Z.to_pos r2).
Lemma Qred_correct : forall q, (Qred q) == q.
Proof.
unfold Qred, Qeq; intros (n,d); simpl.
- generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d))
- (Z.ggcd_correct_divisors n ('d)).
+ generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d))
+ (Z.ggcd_correct_divisors n (Zpos d)).
destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl.
Open Scope Z_scope.
intros Hg LE (Hn,Hd). rewrite Hd, Hn.
@@ -45,13 +45,13 @@ Proof.
unfold Qred, Qeq in *; simpl in *.
Open Scope Z_scope.
intros H.
- generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
- (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+ generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b))
+ (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)).
simpl. intros <- Hg1 Hg2 (Hg3,Hg4).
assert (Hg0 : g <> 0) by (intro; now subst g).
- generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
- (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)).
+ generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d))
+ (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)).
destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)).
simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4).
assert (Hg'0 : g' <> 0) by (intro; now subst g').
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index e4e974972..7c5ddbb6a 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -80,11 +80,11 @@ unfold Qlt.
simpl.
replace (n*1)%Z with n by ring.
ring_simplify.
-replace (n / ' d * ' d + ' d)%Z with
- (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring.
+replace (n / Zpos d * Zpos d + Zpos d)%Z with
+ ((Zpos d * (n / Zpos d) + n mod Zpos d) + Zpos d - n mod Zpos d)%Z by ring.
rewrite <- Z_div_mod_eq; auto with*.
rewrite <- Z.lt_add_lt_sub_r.
-destruct (Z_mod_lt n ('d)); auto with *.
+destruct (Z_mod_lt n (Zpos d)); auto with *.
Qed.
Hint Resolve Qlt_floor : qarith.
@@ -107,9 +107,9 @@ Proof.
intros [xn xd] [yn yd] Hxy.
unfold Qle in *.
simpl in *.
-rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *.
-rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *.
-rewrite (Z.mul_comm ('yd) ('xd)).
+rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *.
+rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *.
+rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).
apply Z_div_le; auto with *.
Qed.
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index 88ab4d6e1..afb78e1c8 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -29,46 +29,34 @@ Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub,
(forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
(forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y).
Proof.
-intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub.
- assert (x_encad : f lb <= x <= f ub).
- split ; [assumption | apply Rle_trans with (r2:=y) ; [apply Rlt_le|] ; assumption].
- assert (y_encad : f lb <= y <= f ub).
- split ; [apply Rle_trans with (r2:=x) ; [|apply Rlt_le] ; assumption | assumption].
- assert (Temp1 : lb <= lb) by intuition ; assert (Temp2 : ub <= ub) by intuition.
- assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)).
- assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)).
- clear Temp1 Temp2.
- case (Rlt_dec (g x) (g y)).
- intuition.
+ intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub.
+ assert (x_encad : f lb <= x <= f ub) by lra.
+ assert (y_encad : f lb <= y <= f ub) by lra.
+ assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)).
+ assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)).
+ case (Rlt_dec (g x) (g y)); [ easy |].
intros Hfalse.
- assert (Temp := Rnot_lt_le _ _ Hfalse).
- assert (Hcontradiction : y <= x).
- replace y with (id y) by intuition ; replace x with (id x) by intuition ;
- rewrite <- f_eq_g. rewrite <- f_eq_g.
- assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y).
+ assert (Temp := Rnot_lt_le _ _ Hfalse).
+ enough (y <= x) by lra.
+ replace y with (id y) by easy.
+ replace x with (id x) by easy.
+ rewrite <- f_eq_g by easy.
+ rewrite <- f_eq_g by easy.
+ assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). {
intros m n lb_le_m m_le_n n_lt_ub.
case (m_le_n).
- intros ; apply Rlt_le ; apply f_incr ; [| | apply Rlt_le] ; assumption.
- intros Hyp ; rewrite Hyp ; apply Req_le ; reflexivity.
- apply f_incr2.
- intuition. intuition.
- Focus 3. intuition.
- Focus 2. intuition.
- Focus 2. intuition. Focus 2. intuition.
- assert (Temp2 : g x <> ub).
- intro Hf.
- assert (Htemp : (comp f g) x = f ub).
- unfold comp ; rewrite Hf ; reflexivity.
- rewrite f_eq_g in Htemp ; unfold id in Htemp.
- assert (Htemp2 : x < f ub).
- apply Rlt_le_trans with (r2:=y) ; intuition.
- clear -Htemp Htemp2. fourier.
- intuition. intuition.
- clear -Temp2 gx_encad.
- case (proj2 gx_encad).
- intuition.
- intro Hfalse ; apply False_ind ; apply Temp2 ; assumption.
- apply False_ind. clear - Hcontradiction x_lt_y. fourier.
+ - intros; apply Rlt_le, f_incr, Rlt_le; assumption.
+ - intros Hyp; rewrite Hyp; apply Req_le; reflexivity.
+ }
+ apply f_incr2; intuition.
+ enough (g x <> ub) by lra.
+ intro Hf.
+ assert (Htemp : (comp f g) x = f ub). {
+ unfold comp; rewrite Hf; reflexivity.
+ }
+ rewrite f_eq_g in Htemp by easy.
+ unfold id in Htemp.
+ fourier.
Qed.
Lemma derivable_pt_id_interv : forall (lb ub x:R),
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index a50140628..a79ddead2 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -11,6 +11,7 @@
(* G. Huet 1-9-95 *)
Require Import Permut Setoid.
+Require Plus. (* comm. and ass. of plus *)
Set Implicit Arguments.
@@ -69,9 +70,6 @@ Section multiset_defs.
unfold meq; unfold munion; simpl; auto.
Qed.
-
- Require Plus. (* comm. and ass. of plus *)
-
Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
Proof.
unfold meq; unfold multiplicity; unfold munion.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 95ba93232..7940bda1a 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -13,7 +13,7 @@
(* G. Huet 1-9-95 *)
(* Updated Papageno 12/98 *)
-Require Import Bool.
+Require Import Bool Permut.
Set Implicit Arguments.
@@ -140,8 +140,6 @@ Hint Resolve seq_right.
(** Here we should make uniset an abstract datatype, by hiding [Charac],
[union], [charac]; all further properties are proved abstractly *)
-Require Import Permut.
-
Lemma union_rotate :
forall x y z:uniset, seq (union x (union y z)) (union z (union x y)).
Proof.
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 8f583be97..d9e5ad676 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -136,7 +136,7 @@ Section defs.
(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
(forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
merge_lem l1 l2.
- Require Import Morphisms.
+ Import Morphisms.
Instance: Equivalence (@meq A).
Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 00:13:40 +0000