From: Enrico Tassi Date: Fri, 27 Jun 2008 16:32:24 +0000 (+0000) Subject: lost in the wood X-Git-Tag: make_still_working~4985 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=052140f5d87dabd49f798b5cf42e35e1df411db3;p=helm.git lost in the wood --- 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 321223710..96cd96e49 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -12,8 +12,65 @@ (* *) (**************************************************************************) +include "nat_ordered_set.ma". include "models/q_bars.ma". +lemma sum_bars_increasing: + ∀l,x.sum_bases l x < sum_bases l (S x). +intro; elim l; +[1: elim x; + [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; + apply q_pos_lt_OQ; + |2: simplify in H ⊢ %; + apply q_lt_plus; rewrite > q_elim_minus; + rewrite < q_plus_assoc; rewrite < q_elim_minus; + rewrite > q_plus_minus; rewrite > q_plus_OQ; + assumption;] +|2: elim x; + [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; + apply q_pos_lt_OQ; + |2: simplify; change in ⊢ (? ? (? % ?)) with (sum_bases l1 (S n)) ; + apply q_lt_plus; rewrite > q_elim_minus; + rewrite < q_plus_assoc; rewrite < q_elim_minus; + rewrite > q_plus_minus; rewrite > q_plus_OQ; apply H]] +qed. + +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; +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_OQ; assumption; +qed. + +lemma sum_bases_lt_canc: + ∀l,x,y.sum_bases l (S x) < sum_bases l (S y) → sum_bases l x < sum_bases l y. +intro; elim l; [apply (q_lt_canc_plus_r ?? (Qpos one));apply H] +generalize in match H1;apply (nat_elim2 (?:? → ? → CProp) ??? x y); +intros 2; +[3: intros 2; simplify; apply q_lt_inj_plus_r; apply H; + apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H3; +|2: cases (?:False); simplify in H2; + apply (q_lt_le_incompat (sum_bases l1 (S n)) OQ);[2: apply sum_bases_ge_OQ;] + apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H2; +|1: cases n in H2; intro; + [1: cases (?:False); apply (q_lt_corefl ? H2); + |2: simplify; apply q_lt_plus_trans; [apply sum_bases_ge_OQ] + apply q_pos_lt_OQ;]] +qed. + +axiom q_minus_distrib: + ∀x,y,z:Q.x - (y + z) = x - y - z. + +axiom q_le_OQ_Qpos: ∀x.OQ ≤ Qpos x. + lemma initial_shift_same_values: ∀l1:q_f.∀init.init < start l1 → same_values l1 @@ -78,15 +135,92 @@ whd in ⊢ (% → ?); simplify in H3; [1: rewrite > H2; do 2 rewrite > q_elim_minus; apply q_lt_plus; rewrite > q_elim_minus; rewrite < q_plus_assoc; rewrite < q_elim_minus; - rewrite > q_plus_minus; - rewrite > q_plus_OQ; assumption; + rewrite > q_plus_minus;rewrite > q_plus_OQ; assumption; |2: rewrite < q_d_noabs; [2: apply q_lt_to_le; assumption] - rewrite > q_d_sym; apply (q_le_S ???? H5); - apply sum_bases_ge_OQ;]] - |3: - - -STOP + rewrite > q_d_sym; apply (q_le_S ???? H5);apply sum_bases_ge_OQ;]] + |3: intro; cases H8; clear H8; rewrite > H11; rewrite > H7; clear H11 H7; + simplify in ⊢ (? ? ? (? ? ? (? ? % ? ?))); + cut (\fst w1 = S (\fst w2)) as Key; [rewrite > Key; reflexivity;] + simplify in H5 H6; + cases (\fst w1) in H5 H6; intros; + [1: cases (?:False); clear H5 H9 H10; simplify in H6; + apply (q_lt_antisym input (start l1)); [2: assumption] + rewrite > q_d_sym in H6; + rewrite > q_d_noabs in H6; [2: apply q_lt_to_le; assumption] + rewrite > q_plus_sym in H6; + rewrite > q_plus_OQ in H6; rewrite > H2 in H6; + lapply (q_lt_plus ??? H6) as X; clear H6 H2 H3 H1 H H4 w1 w2 w; + rewrite > q_elim_minus in X; rewrite < q_plus_assoc in X; + rewrite > (q_plus_sym (Qopp init)) in X; + rewrite < q_elim_minus in X; rewrite > q_plus_minus in X; + rewrite > q_plus_OQ in X; assumption; + |2: simplify in H5; apply eq_f; + cut (sum_bases (bars l1) (\fst w2) < sum_bases (bars l1) (S n)+Qpos w);[2: + apply (q_le_lt_trans ??? H9); + apply (q_lt_trans ??? ? H6); + rewrite > q_d_sym; rewrite > q_d_noabs; [2:apply q_lt_to_le;assumption] + rewrite > q_d_sym; rewrite > q_d_noabs; [2:apply q_lt_to_le;assumption] + do 2 rewrite > q_elim_minus; rewrite > (q_plus_sym ? (Qopp init)); + apply q_lt_plus; rewrite > q_plus_sym; + rewrite > q_elim_minus; rewrite < q_plus_assoc; + rewrite < q_elim_minus; rewrite > q_plus_minus; + rewrite > q_plus_OQ; apply q_lt_opp_opp; assumption] + clear H9 H6; + cut (ⅆ[input,init] - Qpos w = ⅆ[input,start l1]);[2: + rewrite > q_d_sym; rewrite > q_d_noabs; [2:apply q_lt_to_le;assumption] + rewrite > q_d_sym; rewrite > q_d_noabs; [2:apply q_lt_to_le;assumption] + rewrite > H2; rewrite > (q_elim_minus (start ?)); + rewrite > q_minus_distrib; rewrite > q_elim_opp; + do 2 rewrite > q_elim_minus; + do 2 rewrite < q_plus_assoc; + rewrite > (q_plus_sym ? init); + rewrite > (q_plus_assoc ? init); + rewrite > (q_plus_sym ? init); + rewrite < (q_elim_minus init); rewrite > q_plus_minus; + rewrite > (q_plus_sym OQ); rewrite > q_plus_OQ; + rewrite < q_elim_minus; reflexivity;] + cut (sum_bases (bars l1) n < sum_bases (bars l1) (S (\fst w2)));[2: + apply (q_le_lt_trans ???? H10); rewrite < Hcut1; + rewrite > q_elim_minus; apply q_le_minus_r; rewrite > q_elim_opp; + assumption;] clear Hcut1 H5 H10; + generalize in match Hcut;generalize in match Hcut2;clear Hcut Hcut2; + apply (nat_elim2 ???? n (\fst w2)); + [3: intros (x y); apply eq_f; apply H5; clear H5; + [1: clear H7; apply sum_bases_lt_canc; assumption; + |2: clear H6; ] + |2: intros; cases (?:False); clear H6; + cases n1 in H5; intro; + [1: apply (q_lt_corefl ? H5); + |2: cases (bars l1) in H5; intro; + [1: simplify in H5; + apply (q_lt_le_incompat ?? (q_lt_canc_plus_r ??? H5)); + apply q_le_plus_trans; [apply sum_bases_ge_OQ] + apply q_le_OQ_Qpos; + |2: simplify in H5:(??%); + lapply (q_lt_canc_plus_r (sum_bases l (S n2)) ?? H5) as X; + apply (q_lt_le_incompat ?? X); apply sum_bases_ge_OQ]] + |1: intro; cases n1 [intros; reflexivity] intros; cases (?:False); + elim n2 in H5 H6; + + + elim (bars l1) 0; + [1: intro; elim n1; [reflexivity] cases (?:False); + + + intros; clear H5; + elim n1 in H6; [reflexivity] cases (?:False); + [1: apply (q_lt_corefl ? H5); + |2: cases (bars l1) in H5; intro; + [1: simplify in H5; + apply (q_lt_le_incompat ?? (q_lt_canc_plus_r ??? H5)); + apply q_le_plus_trans; [apply sum_bases_ge_OQ] + apply q_le_OQ_Qpos; + |2: simplify in H5:(??%); + lapply (q_lt_canc_plus_r (sum_bases l (S n2)) ?? H5) as X; + apply (q_lt_le_incompat ?? X); apply sum_bases_ge_OQ]] +qed. + + alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". 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 f10113d50..82832c4bc 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_support.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma @@ -51,7 +51,7 @@ 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_opp_opp: ∀a,b.b < a → Qopp a < Qopp 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. @@ -59,6 +59,8 @@ 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_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.