diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-01 14:39:51 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:20 +0200 |
commit | 99be46eb50213d1f35dfc4d30f35760ad5e75621 (patch) | |
tree | 9893c47cf1778fdeede3c2f6e1ec13539ca9ca14 | |
parent | 69aff8116b4878671daf73cc7ccf713aac0c0e6d (diff) |
More proofs independent of the names generated by induction/elim over
a dependent elimination principle for Prop arguments.
-rw-r--r-- | plugins/micromega/ZCoeff.v | 6 | ||||
-rw-r--r-- | theories/FSets/FMapList.v | 24 | ||||
-rw-r--r-- | theories/Lists/ListSet.v | 2 | ||||
-rw-r--r-- | theories/Reals/MVT.v | 47 | ||||
-rw-r--r-- | theories/Reals/RiemannInt_SF.v | 5 |
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; |