aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/micromega/ZCoeff.v6
-rw-r--r--theories/FSets/FMapList.v24
-rw-r--r--theories/Lists/ListSet.v2
-rw-r--r--theories/Reals/MVT.v47
-rw-r--r--theories/Reals/RiemannInt_SF.v5
5 files changed, 42 insertions, 42 deletions
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index e30295e6a..d65c60167 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -41,19 +41,19 @@ Notation "x < y" := (rlt x y).
Lemma req_refl : forall x, req x x.
Proof.
- destruct sor.(SORsetoid).
+ destruct sor.(SORsetoid) as (Equivalence_Reflexive,_,_).
apply Equivalence_Reflexive.
Qed.
Lemma req_sym : forall x y, req x y -> req y x.
Proof.
- destruct sor.(SORsetoid).
+ destruct sor.(SORsetoid) as (_,Equivalence_Symmetric,_).
apply Equivalence_Symmetric.
Qed.
Lemma req_trans : forall x y z, req x y -> req y z -> req x z.
Proof.
- destruct sor.(SORsetoid).
+ destruct sor.(SORsetoid) as (_,_,Equivalence_Transitive).
apply Equivalence_Transitive.
Qed.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index a6f9ae902..13cb559b9 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -403,7 +403,7 @@ Proof.
apply H1 with k; destruct (X.eq_dec x k); auto.
- destruct (X.compare x x'); try contradiction; clear y.
+ destruct (X.compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y.
destruct (H0 x).
assert (In x ((x',e')::l')).
apply H; auto.
@@ -798,7 +798,7 @@ Proof.
intros.
simpl.
destruct a as (k,e); destruct a0 as (k',e').
- destruct (X.compare k k').
+ destruct (X.compare k k') as [Hlt|Heq|Hlt].
inversion_clear Hm.
constructor; auto.
assert (lelistA (ltk (elt:=elt')) (k, e') ((k',e')::m')) by auto.
@@ -922,7 +922,7 @@ Proof.
destruct o; destruct o'; simpl in *; try discriminate; auto.
destruct a as (k,(oo,oo')); simpl in *.
inversion_clear H2.
- destruct (X.compare x k); simpl in *.
+ destruct (X.compare x k) as [Hlt|Heq|Hlt]; simpl in *.
(* x < k *)
destruct (f' (oo,oo')); simpl.
elim_comp.
@@ -958,7 +958,7 @@ Proof.
destruct a as (k,(oo,oo')).
simpl.
inversion_clear H2.
- destruct (X.compare x k).
+ destruct (X.compare x k) as [Hlt|Heq|Hlt].
(* x < k *)
unfold f'; simpl.
destruct (f oo oo'); simpl.
@@ -1207,7 +1207,7 @@ Proof.
destruct a as (x,e).
destruct p as (x',e').
unfold equal; simpl.
- destruct (X.compare x x'); simpl; intuition.
+ destruct (X.compare x x') as [Hlt|Heq|Hlt]; simpl; intuition.
unfold cmp at 1.
MD.elim_comp; clear H; simpl.
inversion_clear Hl.
@@ -1244,7 +1244,7 @@ Lemma eq_refl : forall m : t, eq m m.
Proof.
intros (m,Hm); induction m; unfold eq; simpl; auto.
destruct a.
- destruct (X.compare t0 t0) as [Hlt| |Hlt]; auto.
+ destruct (X.compare t0 t0) as [Hlt|Heq|Hlt]; auto.
apply (MapS.Raw.MX.lt_antirefl Hlt); auto.
split.
apply D.eq_refl.
@@ -1258,7 +1258,7 @@ Proof.
intros (m,Hm); induction m;
intros (m', Hm'); destruct m'; unfold eq; simpl;
try destruct a as (x,e); try destruct p as (x',e'); auto.
- destruct (X.compare x x'); MapS.Raw.MX.elim_comp; intuition.
+ destruct (X.compare x x') as [Hlt|Heq|Hlt]; MapS.Raw.MX.elim_comp; intuition.
inversion_clear Hm; inversion_clear Hm'.
apply (IHm H0 (Build_slist H4)); auto.
Qed.
@@ -1271,8 +1271,8 @@ Proof.
try destruct a as (x,e);
try destruct p as (x',e');
try destruct p0 as (x'',e''); try contradiction; auto.
- destruct (X.compare x x');
- destruct (X.compare x' x'');
+ destruct (X.compare x x') as [Hlt|Heq|Hlt];
+ destruct (X.compare x' x'') as [Hlt'|Heq'|Hlt'];
MapS.Raw.MX.elim_comp; intuition.
apply D.eq_trans with e'; auto.
inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3.
@@ -1287,8 +1287,8 @@ Proof.
try destruct a as (x,e);
try destruct p as (x',e');
try destruct p0 as (x'',e''); try contradiction; auto.
- destruct (X.compare x x');
- destruct (X.compare x' x'');
+ destruct (X.compare x x') as [Hlt|Heq|Hlt];
+ destruct (X.compare x' x'') as [Hlt'|Heq'|Hlt'];
MapS.Raw.MX.elim_comp; intuition.
left; apply D.lt_trans with e'; auto.
left; apply lt_eq with e'; auto.
@@ -1306,7 +1306,7 @@ Proof.
intros (m2, Hm2); destruct m2; unfold eq, lt; simpl;
try destruct a as (x,e);
try destruct p as (x',e'); try contradiction; auto.
- destruct (X.compare x x'); auto.
+ destruct (X.compare x x') as [Hlt|Heq|Hlt]; auto.
intuition.
exact (D.lt_not_eq H0 H1).
inversion_clear Hm1; inversion_clear Hm2.
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 03c2222aa..f02c1d13f 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -116,7 +116,7 @@ Section first_definitions.
simple induction x; simpl; intros.
apply H0; red; trivial.
case (Aeq_dec a a0); auto with datatypes.
- intro; apply H; intros; auto.
+ intro Hneg; apply H; intros; auto.
apply H1; red; intro.
case H3; auto.
Qed.
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 4b8d9af48..e3c5298d7 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -151,14 +151,14 @@ Proof.
cut (forall c:R, a <= c <= b -> continuity_pt id c);
[ intro | intros; apply derivable_continuous_pt; apply derivable_id ].
assert (H2 := MVT f id a b X X0 H H0 H1).
- elim H2; intros c H3; elim H3; intros.
+ destruct H2 as (c & P & H4).
exists c; split.
- cut (derive_pt id c (X0 c x) = derive_pt id c (derivable_pt_id c));
- [ intro | apply pr_nu ].
+ cut (derive_pt id c (X0 c P) = derive_pt id c (derivable_pt_id c));
+ [ intro H5 | apply pr_nu ].
rewrite H5 in H4; rewrite (derive_pt_id c) in H4; rewrite Rmult_1_r in H4;
- rewrite <- H4; replace (derive_pt f c (X c x)) with (derive_pt f c (pr c));
+ rewrite <- H4; replace (derive_pt f c (X c P)) with (derive_pt f c (pr c));
[ idtac | apply pr_nu ]; apply Rmult_comm.
- apply x.
+ apply P.
Qed.
Theorem MVT_cor2 :
@@ -173,14 +173,14 @@ Proof.
intro; cut (forall c:R, a <= c <= b -> derivable_pt id c).
intro X1; cut (forall c:R, a < c < b -> derivable_pt id c).
intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c).
- intro; elim (MVT f id a b X0 X2 H H1 H2); intros; elim H3; clear H3; intros;
- exists x; split.
- cut (derive_pt id x (X2 x x0) = 1).
- cut (derive_pt f x (X0 x x0) = f' x).
+ intro; elim (MVT f id a b X0 X2 H H1 H2); intros x (P,H3).
+ exists x; split.
+ cut (derive_pt id x (X2 x P) = 1).
+ cut (derive_pt f x (X0 x P) = f' x).
intros; rewrite H4 in H3; rewrite H5 in H3; unfold id in H3;
rewrite Rmult_1_r in H3; rewrite Rmult_comm; symmetry ;
assumption.
- apply derive_pt_eq_0; apply H0; elim x0; intros; split; left; assumption.
+ apply derive_pt_eq_0; apply H0; elim P; intros; split; left; assumption.
apply derive_pt_eq_0; apply derivable_pt_lim_id.
assumption.
intros; apply derivable_continuous_pt; apply X1; assumption.
@@ -217,12 +217,12 @@ Proof.
assert (H3 := MVT f id a b pr H2 H0 H);
assert (H4 : forall x:R, a <= x <= b -> continuity_pt id x).
intros; apply derivable_continuous; apply derivable_id.
- elim (H3 H4); intros; elim H5; intros; exists x; exists x0; rewrite H1 in H6;
- unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6;
- rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a);
- [ rewrite Rmult_0_r; apply H6
- | apply Rminus_eq_contra; red; intro; rewrite H7 in H0;
- elim (Rlt_irrefl _ H0) ].
+ destruct (H3 H4) as (c & P & H6). exists c; exists P; rewrite H1 in H6.
+ unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6.
+ rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a);
+ [ rewrite Rmult_0_r; apply H6
+ | apply Rminus_eq_contra; red; intro H7; rewrite H7 in H0;
+ elim (Rlt_irrefl _ H0) ].
Qed.
(**********)
@@ -655,14 +655,15 @@ Proof.
elim H1; intros; apply Rle_trans with x; assumption.
elim H1; clear H1; intros; elim H1; clear H1; intro.
assert (H7 := MVT f id a x H4 H2 H1 H5 H3).
- elim H7; intros; elim H8; intros; assert (H10 : a < x0 < b).
- elim x1; intros; split.
- assumption.
- apply Rlt_le_trans with x; assumption.
- assert (H11 : derive_pt f x0 (H4 x0 x1) = 0).
- replace (derive_pt f x0 (H4 x0 x1)) with (derive_pt f x0 (pr x0 H10));
+ destruct H7 as (c & P & H9).
+ assert (H10 : a < c < b).
+ split.
+ apply P.
+ apply Rlt_le_trans with x; [apply P|assumption].
+ assert (H11 : derive_pt f c (H4 c P) = 0).
+ replace (derive_pt f c (H4 c P)) with (derive_pt f c (pr c H10));
[ apply H0 | apply pr_nu ].
- assert (H12 : derive_pt id x0 (H2 x0 x1) = 1).
+ assert (H12 : derive_pt id c (H2 c P) = 1).
apply derive_pt_eq_0; apply derivable_pt_lim_id.
rewrite H11 in H9; rewrite H12 in H9; rewrite Rmult_0_r in H9;
rewrite Rmult_1_r in H9; apply Rminus_diag_uniq; symmetry ;
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index ef5d37bff..f98b1a143 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -943,9 +943,8 @@ Lemma StepFun_P21 :
forall (a b:R) (f:R -> R) (l:Rlist),
is_subdivision f a b l -> adapted_couple f a b l (FF l f).
Proof.
- intros; unfold adapted_couple; unfold is_subdivision in X;
- unfold adapted_couple in X; elim X; clear X; intros;
- decompose [and] p; clear p; repeat split; try assumption.
+ intros * (x & H & H1 & H0 & H2 & H4).
+ repeat split; try assumption.
apply StepFun_P20; rewrite H2; apply lt_O_Sn.
intros; assert (H5 := H4 _ H3); unfold constant_D_eq, open_interval in H5;
unfold constant_D_eq, open_interval; intros;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 08:58:13 +0000