From d34d7101ba59a19fa030fe9a5c6b3d563efc8f3d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Jul 2008 15:05:26 +0000 Subject: [PATCH 1/1] ... --- .../contribs/dama/dama/models/q_bars.ma | 176 ++++++------------ .../contribs/dama/dama/models/q_support.ma | 88 ++++----- 2 files changed, 102 insertions(+), 162 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma index f75bed7be..2aae66a5b 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -17,137 +17,85 @@ 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 }. +definition 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〉. +definition empty_bar : bar ≝ 〈Qpos 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 [] 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. - -lemma sum_bases_ge_OQ: - ∀l,n. OQ ≤ sum_bases l n. -intro; elim 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. - -alias symbol "leq" = "Q less or equal than". -lemma sum_bases_O: - ∀l.∀x.sum_bases 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 l; -simplify; apply q_lt_plus_trans; -try apply q_pos_lt_OQ; -try apply (sum_bases_ge_OQ []); -apply (sum_bases_ge_OQ l1); -qed. - - -lemma sum_bases_increasing: - ∀l.∀n1,n2:nat.n1 nth_nil; apply (q_pos_OQ one); +|2: cases i in H; [2: cases (?:False); qed. -lemma sum_bases_n_m: - ∀n,m,l. - sum_bases l n < sum_bases l (S m) → - sum_bases l m < sum_bases l (S n) → - n = m. -intros 2; apply (nat_elim2 ???? n m); -[1: intro X; cases X; intros; [reflexivity] cases (?:False); - cases l in H H1; simplify; intros; - apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1)); - apply (q_lt_canc_plus_r ??? H1); -|2: intros 2; cases l; simplify; intros; cases (?:False); - apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1)); - apply (q_lt_canc_plus_r ??? H); (* magia ... *) -|3: intros 4; cases l; simplify; intros; - [1: rewrite > (H []); [reflexivity] - apply (q_lt_canc_plus_r ??(Qpos one)); assumption; - |2: rewrite > (H l1); [reflexivity] - apply (q_lt_canc_plus_r ??(Qpos (\fst b))); assumption;]] -qed. +definition eject_Q ≝ + λP.λp:∃x:ℚ.P x.match p with [ex_introT p _ ⇒ p]. +coercion eject_Q. +definition inject_Q ≝ λP.λp:ℚ.λh:P p. ex_introT ? P p h. +coercion inject_Q with 0 1 nocomposites. -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_spec : q_f → ℚ → ℚ → Prop ≝ + λf,i,q. + ∃j. q = nth_height (bars f) j ∧ + (nth_base (bars f) j < i ∧ + ∀n.j < n → n < len (bars f) → i ≤ nth_base (bars f) n). -definition value : - ∀f:q_f.∀i:ℚ.∃p:nat × ℚ. - Or4 - (And3 (i < start f) (\fst p = O) (\snd p = OQ)) - (And3 - (start f + sum_bases (bars f) (len (bars f)) ≤ i) - (\fst p = O) (\snd p = OQ)) - (And3 (bars f = []) (\fst p = O) (\snd p = OQ)) - (And4 - (And3 (bars f ≠ []) (start f ≤ i) (i < start f + sum_bases (bars f) (len (bars f)))) - (\fst p ≤ (len (bars f))) - (\snd p = \snd (nth (bars f) ▭ (\fst p))) - (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f] ∧ - (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))))). +definition value : ∀f:q_f.∀i:ratio.∃p:ℚ.value_spec f (Qpos i) p. intros; +alias symbol "lt" (instance 5) = "Q less than". +alias symbol "leq" = "Q less or equal than". +letin value_spec_aux ≝ ( + λf,i,q.∃j. q = nth_height f j ∧ + (nth_base f j < i ∧ ∀n.j < n → n < len f → i ≤ nth_base f n)); letin value ≝ ( - let rec value (p: ℚ) (l : list bar) on l ≝ + let rec value (acc: ℚ) (l : list bar) on l : ℚ ≝ match l with - [ nil ⇒ 〈nat_of_q p,OQ〉 + [ nil ⇒ acc | 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〉]] + match q_cmp (\fst x) (Qpos i) with + [ q_leq _ ⇒ value (\snd x) tl + | q_gt _ ⇒ acc]] in value : - ∀acc,l.∃p:nat × ℚ.OQ ≤ acc → - Or - (And3 (l = []) (\fst p = nat_of_q acc) (\snd p = OQ)) - (And3 - (sum_bases l (\fst p) ≤ acc) - (acc < sum_bases l (S (\fst p))) - (\snd p = \snd (nth l ▭ (\fst p))))); + ∀acc,l.∃p:ℚ. OQ ≤ acc → value_spec_aux l (Qpos i) p); +[4: clearbody value; cases (value OQ (bars f)) (p Hp); exists[apply p]; + cases (Hp (q_le_n ?)) (j Hj); cases Hj (Hjp H); cases H (Hin Hmax); + clear Hp value value_spec_aux Hj H; exists [apply j]; split[2:split;intros;] + try apply Hmax; assumption; +|1: intro Hacc; clear H2; cases (value (\snd b) l1) (j Hj); + cases (q_cmp (\snd b) (Qpos i)) (Hib Hib); + [1: cases (Hj Hib) (w Hw); simplify in ⊢ (? ? ? %); clear Hib Hj; + exists [apply (S w)] cases Hw; cases H3; clear Hw H3; + split; try assumption; split; try assumption; intros; + apply (q_le_trans ??? (H5 (pred n) ??)); [3: apply q_le_n] + + + + [5: clearbody value; cases (q_cmp i (start f)); [2: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption; diff --git a/helm/software/matita/contribs/dama/dama/models/q_support.ma b/helm/software/matita/contribs/dama/dama/models/q_support.ma index b948e61b5..6694a033f 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_support.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "Q/q/q.ma". +include "Q/q/qtimes.ma". +include "Q/q/qplus.ma". include "cprop_connectives.ma". notation "\rationals" non associative with precedence 99 for @{'q}. @@ -20,67 +21,61 @@ 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). +interpretation "Q minus" 'minus x y = (qp x (Qopp y)). axiom q_plus_OQ: ∀x:ℚ.x + OQ = x. axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x. axiom q_plus_minus: ∀x.x - 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. -axiom q_elim_minus: ∀x,y.x - y = x + Qopp y. -axiom q_elim_opp: ∀x,y.x - Qopp y = x + y. -axiom q_minus_distrib:∀x,y,z:Q.x - (y + z) = x - y - z. +axiom q_opp_plus: ∀x,y,z:Q. Qopp (y + z) = Qopp y + Qopp z. (* order over Q *) -axiom qlt : ℚ → ℚ → CProp. -axiom qle : ℚ → ℚ → CProp. +axiom qlt : ℚ → ℚ → Prop. +axiom qle : ℚ → ℚ → Prop. 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_leq : 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_le_plus: ∀a,b,c:ℚ. a ≤ c + b → a - b ≤ c. -axiom q_le_plus_r: ∀a,b,c:ℚ. a + b ≤ c → a ≤ c - b. -axiom q_lt_plus_r: ∀a,b,c:ℚ. a + b < c → a < c - b. -axiom q_lt_minus_r: ∀a,b,c:ℚ. a - b < c → a < c + b. +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. + +axiom q_le_plus_l: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c. +axiom q_le_plus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b. +axiom q_lt_plus_l: ∀a,b,c:ℚ. a < c - b → a + b < c. +axiom q_lt_plus_r: ∀a,b,c:ℚ. a - b < c → a < c + b. + axiom q_lt_opp_opp: ∀a,b.b < a → Qopp a < Qopp b. + +axiom q_le_n: ∀x. x ≤ x. 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_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False. -axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False. + +axiom q_neg_gt: ∀r:ratio.Qneg r < OQ. +axiom q_pos_OQ: ∀x.OQ < Qpos x. + axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z. axiom q_lt_le_trans: ∀x,y,z:Q. x < y → y ≤ z → x < z. axiom q_le_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. -axiom q_le_OQ_Qpos: ∀x.OQ ≤ Qpos x. - -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_lt_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y. +axiom q_lt_le_OQ_plus_trans: ∀x,y:Q.OQ < x → OQ ≤ y → OQ < x + y. +axiom q_le_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ ≤ y → OQ ≤ x + y. -axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y. +axiom q_leWl: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z. +axiom q_ltWl: ∀x,y,z.OQ ≤ x → x + y < z → y < z. (* distance *) axiom q_dist : ℚ → ℚ → ℚ. @@ -89,34 +84,32 @@ 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]. +axiom q_d_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y]. +axiom q_d_OQ: ∀x:Q.ⅆ[x,x] = OQ. +axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[y,x] = y - x. +axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x]. -(* integral part *) -axiom nat_of_q: ℚ → nat. +lemma q_2opp: ∀x:ℚ.Qopp (Qopp x) = x. +intros; cases x; reflexivity; qed. (* derived *) lemma q_lt_canc_plus_r: ∀x,y,z:Q.x + z < y + z → x < y. intros; rewrite < (q_plus_OQ y); rewrite < (q_plus_minus z); -rewrite > q_elim_minus; rewrite > q_plus_assoc; -apply q_lt_plus; rewrite > q_elim_opp; assumption; +rewrite > q_plus_assoc; apply q_lt_plus_r; rewrite > q_2opp; assumption; qed. lemma q_lt_inj_plus_r: ∀x,y,z:Q.x < y → x + z < y + z. intros; apply (q_lt_canc_plus_r ?? (Qopp z)); -do 2 (rewrite < q_plus_assoc;rewrite < q_elim_minus); -rewrite > q_plus_minus; +do 2 rewrite < q_plus_assoc; rewrite > q_plus_minus; do 2 rewrite > q_plus_OQ; assumption; qed. lemma q_le_inj_plus_r: ∀x,y,z:Q.x ≤ y → x + z ≤ y + z. intros;cases (q_le_cases ?? H); -[1: rewrite > H1; apply q_eq_to_le; reflexivity; +[1: rewrite > H1; apply q_le_n; |2: apply q_lt_to_le; apply q_lt_inj_plus_r; assumption;] qed. @@ -124,6 +117,5 @@ lemma q_le_canc_plus_r: ∀x,y,z:Q.x + z ≤ y + z → x ≤ y. intros; lapply (q_le_inj_plus_r ?? (Qopp z) H) as H1; do 2 rewrite < q_plus_assoc in H1; -rewrite < q_elim_minus in H1; rewrite > q_plus_minus in H1; -do 2 rewrite > q_plus_OQ in H1; assumption; +rewrite > q_plus_minus in H1; do 2 rewrite > q_plus_OQ in H1; assumption; qed. -- 2.39.2