From f1a90ee8745c3fa5324e7a7e8c2f8398483c1ff6 Mon Sep 17 00:00:00 2001 From: Enrico Zoli Date: Fri, 3 Nov 2006 11:15:03 +0000 Subject: [PATCH] Up to max (up to a bug). --- .../matita/dama/constructive_connectives.ma | 13 +++- helm/software/matita/dama/groups.ma | 24 ++++++ .../matita/dama/ordered_fields_ch0.ma | 15 +++- helm/software/matita/dama/reals.ma | 73 +++++++++++++------ 4 files changed, 99 insertions(+), 26 deletions(-) diff --git a/helm/software/matita/dama/constructive_connectives.ma b/helm/software/matita/dama/constructive_connectives.ma index 259357934..461f90e6d 100644 --- a/helm/software/matita/dama/constructive_connectives.ma +++ b/helm/software/matita/dama/constructive_connectives.ma @@ -18,6 +18,17 @@ inductive or (A,B:Type) : Type \def Left : A → or A B | Right : B → or A B. -interpretation "classical or" 'or x y = +interpretation "constructive or" 'or x y = (cic:/matita/constructive_connectives/or.ind#xpointer(1/1) x y). +inductive ex (A:Type) (P:A→Prop) : Type \def + ex_intro: ∀w:A. P w → ex A P. + +notation < "hvbox(Σ ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'exists ${default + @{\lambda ${ident i} : $ty. $p)} + @{\lambda ${ident i} . $p}}}. + +interpretation "constructive exists" 'sigma \eta.x = + (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x). \ No newline at end of file diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma index 6d832c208..1b39c1518 100644 --- a/helm/software/matita/dama/groups.ma +++ b/helm/software/matita/dama/groups.ma @@ -103,3 +103,27 @@ rewrite > zero_neutral in H1; assumption. qed. +theorem eq_opp_plus_plus_opp_opp: ∀G:abelian_group.∀x,y:G. -(x+y) = -x + -y. + intros; + apply (cancellationlaw ? (x+y)); + rewrite < plus_comm; + rewrite > opp_inverse; + rewrite > plus_assoc; + rewrite > plus_comm in ⊢ (? ? ? (? ? ? (? ? ? %))); + rewrite < plus_assoc in ⊢ (? ? ? (? ? ? %)); + rewrite > plus_comm; + rewrite > plus_comm in ⊢ (? ? ? (? ? (? ? % ?) ?)); + rewrite > opp_inverse; + rewrite > zero_neutral; + rewrite > opp_inverse; + reflexivity. +qed. + +theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x=x. + intros; + apply (cancellationlaw ? (-x)); + rewrite > opp_inverse; + rewrite > plus_comm; + rewrite > opp_inverse; + reflexivity. +qed. \ No newline at end of file diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma index f796ebb1d..c7bf906f5 100644 --- a/helm/software/matita/dama/ordered_fields_ch0.ma +++ b/helm/software/matita/dama/ordered_fields_ch0.ma @@ -21,6 +21,17 @@ record is_total_order_relation (C:Type) (le:C→C→Prop) : Type \def to_antisimmetry: ∀x,y:C. le x y → le y x → x=y }. +theorem to_transitive: ∀C,le. is_total_order_relation C le → transitive ? le. + intros; + unfold transitive; + intros; + elim (to_cotransitive ? ? i ? ? z H); + [ assumption + | rewrite < (to_antisimmetry ? ? i ? ? H1 t); + assumption + ]. +qed. + record is_ordered_field_ch0 (F:field) (le:F→F→Prop) : Type \def { of_total_order_relation:> is_total_order_relation ? le; of_mult_compat: ∀a,b. le 0 a → le 0 b → le 0 (a*b); @@ -105,6 +116,8 @@ definition is_cauchy_seq ≝ -eps ≤ f M - f n ∧ f M - f n ≤ eps. *) + + definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop. apply (λF:ordered_field_ch0.λf:nat→F. @@ -120,4 +133,4 @@ qed. definition is_complete ≝ λF:ordered_field_ch0. ∀f:nat→F. is_cauchy_seq ? f → - ∃l:F. tends_to ? f l. \ No newline at end of file + ex F (λl:F. tends_to ? f l). \ No newline at end of file diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma index 5566ece43..f587435a3 100644 --- a/helm/software/matita/dama/reals.ma +++ b/helm/software/matita/dama/reals.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/reals/". include "ordered_fields_ch0.ma". -record is_real (F:ordered_field_ch0) : Prop +record is_real (F:ordered_field_ch0) : Type ≝ { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field F n); r_complete: is_complete F @@ -46,48 +46,73 @@ definition max_seq: ∀R:real.∀x,y:R. nat → R. ]. qed. +axiom daemon: False. + theorem cauchy_max_seq: ∀R:real.∀x,y. is_cauchy_seq ? (max_seq R x y). intros; unfold; intros; - apply (ex_intro ? ? m); + exists; [ exact m | ]; (* apply (ex_intro ? ? m); *) intros; - split; - [ - | unfold max_seq; - elim (to_cotransitive R (of_le R) R 0 + unfold max_seq; + elim (to_cotransitive R (of_le R) R 0 (inv R (sum_field R (S N)) (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N)))) (x-y) (lt_zero_to_le_inv_zero R (S N) (not_eq_sum_field_zero R (S N) (le_S_S O N (le_O_n N))))); - [ simplify; - elim (to_cotransitive R (of_le R) R 0 + [ simplify; + elim (to_cotransitive R (of_le R) R 0 (inv R (1+sum R (plus R) 0 1 m) (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y) (lt_zero_to_le_inv_zero R (S m) (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m))))); - [ simplify; - rewrite > (plus_comm ? x (-x)); - rewrite > opp_inverse; - apply lt_zero_to_le_inv_zero - | simplify; - assumption + [ simplify; + rewrite > (plus_comm ? x (-x)); + rewrite > opp_inverse; + split; + [ elim daemon (* da finire *) + | apply lt_zero_to_le_inv_zero + ] + | simplify; + split; + [ elim daemon (* da finire *) + | assumption ] - | elim (to_cotransitive R (of_le R) R 0 + ] + | simplify; + elim (to_cotransitive R (of_le R) R 0 (inv R (1+sum R (plus R) 0 1 m) (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m)))) (x-y) (lt_zero_to_le_inv_zero R (S m) (not_eq_sum_field_zero R (S m) (le_S_S O m (le_O_n m))))); - [ simplify; - generalize in match (le_zero_x_to_le_opp_x_zero R ? t1); - intro; - (* finire *) - |simplify; - rewrite > (plus_comm ? y (-y)); - rewrite > opp_inverse; - apply lt_zero_to_le_inv_zero + [ simplify; + split; + [ elim daemon (* da finire *) + | generalize in match (le_zero_x_to_le_opp_x_zero R ? t1); + intro; + unfold minus in H1; + rewrite > eq_opp_plus_plus_opp_opp in H1; + rewrite > eq_opp_opp_x_x in H1; + rewrite > plus_comm in H1; + apply (to_transitive ? ? (of_total_order_relation ? ? R) ? 0 ?); + [ assumption + | apply lt_zero_to_le_inv_zero + ] ] + | simplify; + rewrite > (plus_comm ? y (-y)); + rewrite > opp_inverse; + split; + [ elim daemon (* da finire *) + | apply lt_zero_to_le_inv_zero + ] ] ]. +qed. + +definition max: ∀R:real.R → R → R. + intros (R x y); + elim (r_complete ? (r_real_properties R) ? ?); + [|| apply (cauchy_max_seq R x y) ] +qed. - \ No newline at end of file -- 2.39.2