diff options
| -rw-r--r-- | plugins/rtauto/Rtauto.v | 225 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis5.v | 62 |
2 files changed, 134 insertions, 153 deletions
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index f951df26a..06542b526 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -255,122 +255,115 @@ Theorem interp_proof: forall p hyps F gl, check_proof hyps gl p = true -> interp_ctx hyps F [[gl]]. -induction p;intros hyps F gl. - -(* cas Axiom *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f nth_f e;rewrite <- (form_eq_refl e). -apply project with p;trivial. - -(* Cas Arrow_Intro *) -Focus 1. -destruct gl;clean. -simpl;intros. -change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). -apply IHp;try constructor;trivial. - -(* Cas Arrow_Elim *) -Focus 1. -simpl check_proof;case_eq (get p hyps);clean. -intros f ef;case_eq (get p0 hyps);clean. -intros f0 ef0;destruct f0;clean. -case_eq (form_eq f f0_1);clean. -simpl;intros e check_p1. -generalize (project F ef) (project F ef0) -(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); -clear check_p1 IHp p p0 p1 ef ef0. -simpl. -apply compose3. -rewrite (form_eq_refl e). -auto. - -(* cas Arrow_Destruct *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean. -intros check_p1 check_p2. -generalize (project F ef) -(IHp1 (hyps \ f1_2 =>> f2 \ f1_1) -(F_push f1_1 (hyps \ f1_2 =>> f2) - (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). -simpl;apply compose3;auto. - -(* Cas False_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intros _; generalize (project F ef). -apply compose1;apply False_ind. - -(* Cas And_Intro *) -Focus 1. -simpl;destruct gl;clean. -case_eq (check_proof hyps gl1 p1);clean. -intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). -apply compose2 ;simpl;auto. - -(* cas And_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intro check_p;generalize (project F ef) -(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). -simpl;apply compose2;intros [h1 h2];auto. - -(* cas And_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro H;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f1_2 =>> f2) -(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl. -apply compose2;auto. - -(* cas Or_Intro_left *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl1 Hp). -apply compose1;simpl;auto. - -(* cas Or_Intro_right *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl2 Hp). -apply compose1;simpl;auto. - -(* cas Or_elim *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -case_eq (check_proof (hyps \ f1) gl p2);clean. -intros check_p1 check_p2;generalize (project F ef) -(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); -simpl;apply compose3;simpl;intro h;destruct h;auto. - -(* cas Or_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro check_p0;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) -(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) - (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl. -apply compose2;auto. - -(* cas Cut *) -Focus 1. -simpl;case_eq (check_proof hyps f p1);clean. -intros check_p1 check_p2; -generalize (IHp1 hyps F f check_p1) -(IHp2 (hyps\f) (F_push f hyps F) gl check_p2); -simpl; apply compose2;auto. +induction p; intros hyps F gl. + +- (* Axiom *) + simpl;case_eq (get p hyps);clean. + intros f nth_f e;rewrite <- (form_eq_refl e). + apply project with p;trivial. + +- (* Arrow_Intro *) + destruct gl; clean. + simpl; intros. + change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). + apply IHp; try constructor; trivial. + +- (* Arrow_Elim *) + simpl check_proof; case_eq (get p hyps); clean. + intros f ef; case_eq (get p0 hyps); clean. + intros f0 ef0; destruct f0; clean. + case_eq (form_eq f f0_1); clean. + simpl; intros e check_p1. + generalize (project F ef) (project F ef0) + (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); + clear check_p1 IHp p p0 p1 ef ef0. + simpl. + apply compose3. + rewrite (form_eq_refl e). + auto. + +- (* Arrow_Destruct *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2); clean. + intros check_p1 check_p2. + generalize (project F ef) + (IHp1 (hyps \ f1_2 =>> f2 \ f1_1) + (F_push f1_1 (hyps \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). + simpl; apply compose3; auto. + +- (* False_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intros _; generalize (project F ef). + apply compose1; apply False_ind. + +- (* And_Intro *) + simpl; destruct gl; clean. + case_eq (check_proof hyps gl1 p1); clean. + intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). + apply compose2 ; simpl; auto. + +- (* And_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intro check_p; + generalize (project F ef) + (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). + simpl; apply compose2; intros [h1 h2]; auto. + +- (* And_Destruct*) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro H; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f1_2 =>> f2) + (F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H); + clear H; simpl. + apply compose2; auto. + +- (* Or_Intro_left *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl1 Hp). + apply compose1; simpl; auto. + +- (* Or_Intro_right *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl2 Hp). + apply compose1; simpl; auto. + +- (* Or_elim *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + case_eq (check_proof (hyps \ f1) gl p2); clean. + intros check_p1 check_p2; + generalize (project F ef) + (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); + simpl; apply compose3; simpl; intro h; destruct h; auto. + +- (* Or_Destruct *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro check_p0; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) + (F_push (f1_1 =>> f2) hyps F)) gl check_p0); + simpl. + apply compose2; auto. + +- (* Cut *) + simpl; case_eq (check_proof hyps f p1); clean. + intros check_p1 check_p2; + generalize (IHp1 hyps F f check_p1) + (IHp2 (hyps\f) (F_push f hyps F) gl check_p2); + simpl; apply compose2; auto. Qed. Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True. diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index 61c0debb7..de1e2f303 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -27,46 +27,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), |