From: Enrico Tassi Date: Thu, 26 Jun 2008 20:22:19 +0000 (+0000) Subject: more work X-Git-Tag: make_still_working~4988 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f8f3f0bf31de02f543b9bb5e944ea01fd706d3a0;p=helm.git more work --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 7bd17218a..559194e76 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,24 +1,27 @@ +sandwich.ma ordered_uniform.ma +property_sigma.ma ordered_uniform.ma russell_support.ma +uniform.ma supremum.ma bishop_set.ma ordered_set.ma -ordered_set.ma cprop_connectives.ma -cprop_connectives.ma logic/equality.ma -bishop_set_rewrite.ma bishop_set.ma sequence.ma nat/nat.ma -uniform.ma supremum.ma -supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma -nat_ordered_set.ma bishop_set.ma nat/compare.ma -property_sigma.ma ordered_uniform.ma russell_support.ma ordered_uniform.ma uniform.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma property_exhaustivity.ma ordered_uniform.ma property_sigma.ma +bishop_set_rewrite.ma bishop_set.ma +cprop_connectives.ma datatypes/constructors.ma logic/equality.ma +nat_ordered_set.ma bishop_set.ma nat/compare.ma lebesgue.ma property_exhaustivity.ma sandwich.ma -sandwich.ma ordered_uniform.ma +ordered_set.ma cprop_connectives.ma russell_support.ma cprop_connectives.ma nat/nat.ma -models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma +models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma -models/q_function.ma Q/q/q.ma cprop_connectives.ma list/list.ma +models/q_support.ma Q/q/q.ma models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma -models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma -models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma +models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma +models/q_function.ma models/q_bars.ma models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma +models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma +models/list_support.ma list/list.ma +models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma Q/q/q.ma datatypes/constructors.ma list/list.ma diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png index a45e35369..0365b1fad 100644 Binary files a/helm/software/matita/contribs/dama/dama/depends.png and b/helm/software/matita/contribs/dama/dama/depends.png differ diff --git a/helm/software/matita/contribs/dama/dama/models/list_support.ma b/helm/software/matita/contribs/dama/dama/models/list_support.ma new file mode 100644 index 000000000..d9188b0a6 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/list_support.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "list/list.ma". + +interpretation "list nth" 'nth = (nth _). +interpretation "list nth" 'nth_appl l d i = (nth _ l d i). +notation "'nth'" with precedence 90 for @{'nth}. +notation < "'nth' \nbsp term 90 l \nbsp term 90 d \nbsp term 90 i" +with precedence 69 for @{'nth_appl $l $d $i}. + +definition make_list ≝ + λA:Type.λdef:nat→A. + let rec make_list (n:nat) on n ≝ + match n with [ O ⇒ nil ? | S m ⇒ def m :: make_list m] + in make_list. + +interpretation "'mk_list' appl" 'mk_list_appl f n = (make_list _ f n). +interpretation "'mk_list'" 'mk_list = (make_list _). +notation "'mk_list'" with precedence 90 for @{'mk_list}. +notation < "'mk_list' \nbsp term 90 f \nbsp term 90 n" +with precedence 69 for @{'mk_list_appl $f $n}. + +notation "'len'" with precedence 90 for @{'len}. +interpretation "len" 'len = (length _). +notation < "'len' \nbsp term 90 l" with precedence 69 for @{'len_appl $l}. +interpretation "len appl" 'len_appl l = (length _ l). + +lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.len (mk_list f n) = n. +intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity; +qed. + diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma new file mode 100644 index 000000000..249abdf6c --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -0,0 +1,150 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "models/q_support.ma". +include "models/list_support.ma". +include "cprop_connectives.ma". + +definition bar ≝ ratio × ℚ. (* base (Qpos) , height *) +record q_f : Type ≝ { start : ℚ; bars: list bar }. + +notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}. +interpretation "Q x Q" 'q2 = (Prod Q Q). + +definition empty_bar : bar ≝ 〈one,OQ〉. +notation "\rect" with precedence 90 for @{'empty_bar}. +interpretation "q0" 'empty_bar = empty_bar. + +notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}. +interpretation "lq2" 'lq2 = (list bar). + +let rec sum_bases (l:list bar) (i:nat)on i ≝ + match i with + [ O ⇒ OQ + | S m ⇒ + match l with + [ nil ⇒ sum_bases l m + Qpos one + | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]]. + +axiom sum_bases_empty_nat_of_q_ge_OQ: + ∀q:ℚ.OQ ≤ sum_bases [] (nat_of_q q). +axiom sum_bases_empty_nat_of_q_le_q: + ∀q:ℚ.sum_bases [] (nat_of_q q) ≤ q. +axiom sum_bases_empty_nat_of_q_le_q_one: + ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one. + +definition eject1 ≝ + λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p]. +coercion eject1. +definition inject1 ≝ λP.λp:nat × ℚ.λh:P p. ex_introT ? P p h. +coercion inject1 with 0 1 nocomposites. + +definition value : + ∀f:q_f.∀i:ℚ.∃p:nat × ℚ. + match q_cmp i (start f) with + [ q_lt _ ⇒ \snd p = OQ + | _ ⇒ + And3 + (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f]) + (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))) + (\snd p = \snd (nth (bars f) ▭ (\fst p)))]. +intros; +alias symbol "pi2" = "pair pi2". +alias symbol "pi1" = "pair pi1". +letin value ≝ ( + let rec value (p: ℚ) (l : list bar) on l ≝ + match l with + [ nil ⇒ 〈nat_of_q p,OQ〉 + | cons x tl ⇒ + match q_cmp p (Qpos (\fst x)) with + [ q_lt _ ⇒ 〈O, \snd x〉 + | _ ⇒ + let rc ≝ value (p - Qpos (\fst x)) tl in + 〈S (\fst rc),\snd rc〉]] + in value : + ∀acc,l.∃p:nat × ℚ. OQ ≤ acc → + And3 + (sum_bases l (\fst p) ≤ acc) + (acc < sum_bases l (S (\fst p))) + (\snd p = \snd (nth l ▭ (\fst p)))); +[5: clearbody value; + cases (q_cmp i (start f)); + [2: exists [apply 〈O,OQ〉] simplify; reflexivity; + |*: cases (value ⅆ[i,start f] (bars f)) (p Hp); + cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; + exists[1,3:apply p]; simplify; split; assumption;] +|1,3: intros; split; + [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); + cases (H2 (q_le_to_diff_ge_OQ ?? (? H1))); + [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption] + simplify; apply q_le_minus; assumption; + |2,5: cases (value (q-Qpos (\fst b)) l1); + cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); + [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption] + clear H3 H2 value; + change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b)); + apply q_lt_plus; assumption; + |*: cases (value (q-Qpos (\fst b)) l1); simplify; + cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); + [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption] + assumption;] +|2: clear value H2; simplify; intros; split; [assumption|3:reflexivity] + rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption; +|4: simplify; intros; split; + [1: apply sum_bases_empty_nat_of_q_le_q; + |2: apply sum_bases_empty_nat_of_q_le_q_one; + |3: elim (nat_of_q q); [reflexivity] simplify; assumption]] +qed. + + +definition same_values ≝ + λl1,l2:q_f. + ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). + +definition same_bases ≝ + λl1,l2:q_f. + (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)). + +alias symbol "lt" = "Q less than". +lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x. +intro; cases x; intros; [2:exists [apply r] reflexivity] +cases (?:False); +[ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)] +qed. + +notation < "\blacksquare" non associative with precedence 90 for @{'hide}. +definition hide ≝ λT:Type.λx:T.x. +interpretation "hide" 'hide = (hide _ _). + +lemma sum_bases_ge_OQ: + ∀l,n. OQ ≤ sum_bases (bars l) n. +intro; elim (bars l); simplify; intros; +[1: elim n; [apply q_eq_to_le;reflexivity] simplify; + apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ; +|2: cases n; [apply q_eq_to_le;reflexivity] simplify; + apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]] +qed. + +lemma sum_bases_O: + ∀l:q_f.∀x.sum_bases (bars l) x ≤ OQ → x = O. +intros; cases x in H; [intros; reflexivity] intro; cases (?:False); +cases (q_le_cases ?? H); +[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); +|2: apply (q_lt_antisym ??? H1);] clear H H1; cases (bars l); +simplify; apply q_lt_plus_trans; +try apply q_pos_lt_OQ; +try apply (sum_bases_ge_OQ (mk_q_f OQ [])); +apply (sum_bases_ge_OQ (mk_q_f OQ l1)); +qed. + diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma index 5d642228d..624755ed7 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -12,230 +12,7 @@ (* *) (**************************************************************************) -include "Q/q/q.ma". -include "list/list.ma". -include "cprop_connectives.ma". - - -notation "\rationals" non associative with precedence 99 for @{'q}. -interpretation "Q" 'q = Q. - -definition bar ≝ ratio × ℚ. (* base (Qpos) , height *) -record q_f : Type ≝ { start : ℚ; bars: list bar }. - -axiom qp : ℚ → ℚ → ℚ. -axiom qm : ℚ → ℚ → ℚ. -axiom qlt : ℚ → ℚ → CProp. - -interpretation "Q plus" 'plus x y = (qp x y). -interpretation "Q minus" 'minus x y = (qm x y). -interpretation "Q less than" 'lt x y = (qlt x y). - -inductive q_comparison (a,b:ℚ) : CProp ≝ - | q_eq : a = b → q_comparison a b - | q_lt : a < b → q_comparison a b - | q_gt : b < a → q_comparison a b. - -axiom q_cmp:∀a,b:ℚ.q_comparison a b. - -definition qle ≝ λa,b:ℚ.a = b ∨ a < b. - -interpretation "Q less or equal than" 'leq x y = (qle x y). - -axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c. -axiom q_le_minus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b. -axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b. -axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b. - -axiom q_dist : ℚ → ℚ → ℚ. - -notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90 -for @{'distance $x $y}. -interpretation "ℚ distance" 'distance x y = (q_dist x y). - -axiom q_dist_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y]. - -axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b. -axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a. -axiom q_plus_OQ: ∀x:ℚ.x + OQ = x. -axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x. -axiom nat_of_q: ℚ → nat. - -interpretation "list nth" 'nth = (nth _). -interpretation "list nth" 'nth_appl l d i = (nth _ l d i). -notation "'nth'" with precedence 90 for @{'nth}. -notation < "'nth' \nbsp term 90 l \nbsp term 90 d \nbsp term 90 i" -with precedence 69 for @{'nth_appl $l $d $i}. - -notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}. -interpretation "Q x Q" 'q2 = (Prod Q Q). - -definition make_list ≝ - λA:Type.λdef:nat→A. - let rec make_list (n:nat) on n ≝ - match n with [ O ⇒ nil ? | S m ⇒ def m :: make_list m] - in make_list. - -interpretation "'mk_list' appl" 'mk_list_appl f n = (make_list _ f n). -interpretation "'mk_list'" 'mk_list = (make_list _). -notation "'mk_list'" with precedence 90 for @{'mk_list}. -notation < "'mk_list' \nbsp term 90 f \nbsp term 90 n" -with precedence 69 for @{'mk_list_appl $f $n}. - - -definition empty_bar : bar ≝ 〈one,OQ〉. -notation "\rect" with precedence 90 for @{'empty_bar}. -interpretation "q0" 'empty_bar = empty_bar. - -notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}. -interpretation "lq2" 'lq2 = (list bar). - -notation "'len'" with precedence 90 for @{'len}. -interpretation "len" 'len = (length _). -notation < "'len' \nbsp term 90 l" with precedence 69 for @{'len_appl $l}. -interpretation "len appl" 'len_appl l = (length _ l). - -lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.len (mk_list f n) = n. -intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity; -qed. - -let rec sum_bases (l:list bar) (i:nat)on i ≝ - match i with - [ O ⇒ OQ - | S m ⇒ - match l with - [ nil ⇒ sum_bases l m + Qpos one - | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]]. - -axiom sum_bases_empty_nat_of_q_ge_OQ: - ∀q:ℚ.OQ ≤ sum_bases [] (nat_of_q q). -axiom sum_bases_empty_nat_of_q_le_q: - ∀q:ℚ.sum_bases [] (nat_of_q q) ≤ q. -axiom sum_bases_empty_nat_of_q_le_q_one: - ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one. - -definition eject1 ≝ - λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p]. -coercion eject1. -definition inject1 ≝ λP.λp:nat × ℚ.λh:P p. ex_introT ? P p h. -coercion inject1 with 0 1 nocomposites. - -definition value : - ∀f:q_f.∀i:ℚ.∃p:nat × ℚ. - match q_cmp i (start f) with - [ q_lt _ ⇒ \snd p = OQ - | _ ⇒ - And3 - (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f]) - (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))) - (\snd p = \snd (nth (bars f) ▭ (\fst p)))]. -intros; -alias symbol "pi2" = "pair pi2". -alias symbol "pi1" = "pair pi1". -letin value ≝ ( - let rec value (p: ℚ) (l : list bar) on l ≝ - match l with - [ nil ⇒ 〈nat_of_q p,OQ〉 - | cons x tl ⇒ - match q_cmp p (Qpos (\fst x)) with - [ q_lt _ ⇒ 〈O, \snd x〉 - | _ ⇒ - let rc ≝ value (p - Qpos (\fst x)) tl in - 〈S (\fst rc),\snd rc〉]] - in value : - ∀acc,l.∃p:nat × ℚ. OQ ≤ acc → - And3 - (sum_bases l (\fst p) ≤ acc) - (acc < sum_bases l (S (\fst p))) - (\snd p = \snd (nth l ▭ (\fst p)))); -[5: clearbody value; - cases (q_cmp i (start f)); - [2: exists [apply 〈O,OQ〉] simplify; reflexivity; - |*: cases (value ⅆ[i,start f] (bars f)) (p Hp); - cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; - exists[1,3:apply p]; simplify; split; assumption;] -|1,3: intros; split; - [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); - cases (H2 (q_le_to_diff_ge_OQ ?? (? H1))); - [1,3: intros; [right|left;symmetry] assumption] - simplify; apply q_le_minus; assumption; - |2,5: cases (value (q-Qpos (\fst b)) l1); - cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); - [1,3: intros; [right|left;symmetry] assumption] - clear H3 H2 value; - change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b)); - apply q_lt_plus; assumption; - |*: cases (value (q-Qpos (\fst b)) l1); simplify; - cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); - [1,3: intros; [right|left;symmetry] assumption] - assumption;] -|2: clear value H2; simplify; intros; split; [assumption|3:reflexivity] - rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption; -|4: simplify; intros; split; - [1: apply sum_bases_empty_nat_of_q_le_q; - |2: apply sum_bases_empty_nat_of_q_le_q_one; - |3: elim (nat_of_q q); [reflexivity] simplify; assumption]] -qed. - - -definition same_values ≝ - λl1,l2:q_f. - ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). - -definition same_bases ≝ - λl1,l2:q_f. - (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)). - -axiom q_lt_corefl: ∀x:Q.x < x → False. -axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False. -axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False. -axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ. -axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False. -axiom q_lt_plus_trans: - ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y. -axiom q_pos_lt_OQ: ∀x.OQ < Qpos x. -axiom q_le_plus_trans: - ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y. -axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z. -axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z. -axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[x,y] = y - x. -axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x]. -axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z. -axiom q_plus_minus: ∀x.Qpos x + Qneg x = OQ. -axiom q_minus: ∀x,y. y - Qpos x = y + Qneg x. -axiom q_minus_r: ∀x,y. y + Qpos x = y - Qneg x. -axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z. - -lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x. -intro; cases x; intros; [2:exists [apply r] reflexivity] -cases (?:False); -[ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)] -qed. - -notation < "\blacksquare" non associative with precedence 90 for @{'hide}. -definition hide ≝ λT:Type.λx:T.x. -interpretation "hide" 'hide = (hide _ _). - -lemma sum_bases_ge_OQ: - ∀l,n. OQ ≤ sum_bases (bars l) n. -intro; elim (bars l); simplify; intros; -[1: elim n; [left;reflexivity] simplify; - apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ; -|2: cases n; [left;reflexivity] simplify; - apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]] -qed. - -lemma sum_bases_O: - ∀l:q_f.∀x.sum_bases (bars l) x ≤ OQ → x = O. -intros; cases x in H; [intros; reflexivity] intro; cases (?:False); -cases H; -[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); -|2: apply (q_lt_antisym ??? H1);] clear H H1; cases (bars l); -simplify; apply q_lt_plus_trans; -try apply q_pos_lt_OQ; -try apply (sum_bases_ge_OQ (mk_q_f OQ [])); -apply (sum_bases_ge_OQ (mk_q_f OQ l1)); -qed. +include "models/q_bars.ma". lemma initial_shift_same_values: ∀l1:q_f.∀init.init < start l1 → @@ -397,4 +174,4 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; |6:(* TODO *) |7:(* TODO *) |8: intros; cases (?:False); apply (not_le_Sn_O ? H1);] -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/contribs/dama/dama/models/q_support.ma b/helm/software/matita/contribs/dama/dama/models/q_support.ma new file mode 100644 index 000000000..4b80d92cf --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Q/q/q.ma". +include "cprop_connectives.ma". + +notation "\rationals" non associative with precedence 99 for @{'q}. +interpretation "Q" 'q = Q. + +(* group over Q *) +axiom qp : ℚ → ℚ → ℚ. +axiom qm : ℚ → ℚ → ℚ. + +interpretation "Q plus" 'plus x y = (qp x y). +interpretation "Q minus" 'minus x y = (qm x y). + +axiom q_plus_OQ: ∀x:ℚ.x + OQ = x. +axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x. +axiom q_plus_minus: ∀x.Qpos x + Qneg x = OQ. +axiom q_minus: ∀x,y. y - Qpos x = y + Qneg x. +axiom q_minus_r: ∀x,y. y + Qpos x = y - Qneg x. +axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z. + +(* order over Q *) +axiom qlt : ℚ → ℚ → CProp. +axiom qle : ℚ → ℚ → CProp. +interpretation "Q less than" 'lt x y = (qlt x y). +interpretation "Q less or equal than" 'leq x y = (qle x y). + +inductive q_comparison (a,b:ℚ) : CProp ≝ + | q_eq : a = b → q_comparison a b + | q_lt : a < b → q_comparison a b + | q_gt : b < a → q_comparison a b. + +axiom q_cmp:∀a,b:ℚ.q_comparison a b. + +axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c. +axiom q_le_minus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b. +axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b. +axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b. + +axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b. +axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a. +axiom q_lt_corefl: ∀x:Q.x < x → False. +axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False. +axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False. +axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z. +axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z. +axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False. +axiom q_lt_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y. +axiom q_pos_lt_OQ: ∀x.OQ < Qpos x. +axiom q_le_plus_trans: ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y. +axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z. +axiom q_eq_to_le: ∀x,y. x = y → x ≤ y. + +inductive q_le_elimination (a,b:ℚ) : CProp ≝ +| q_le_from_eq : a = b → q_le_elimination a b +| q_le_from_lt : a < b → q_le_elimination a b. + +axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y. + +(* distance *) +axiom q_dist : ℚ → ℚ → ℚ. + +notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90 +for @{'distance $x $y}. +interpretation "ℚ distance" 'distance x y = (q_dist x y). + +axiom q_dist_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y]. +axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ. +axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[x,y] = y - x. +axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x]. + +(* integral part *) +axiom nat_of_q: ℚ → nat. +