From: Enrico Tassi Date: Fri, 27 Jun 2008 19:11:42 +0000 (+0000) Subject: more work to try to understand where the issue is X-Git-Tag: make_still_working~4984 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88b32d4e8fe371d59e41cd272064c9d486ae7ec5;p=helm.git more work to try to understand where the issue is --- 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 6be729db5..d0d043f47 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -29,7 +29,7 @@ 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 ≝ +let rec sum_bases (l:list bar) (i:nat) on i ≝ match i with [ O ⇒ OQ | S m ⇒ @@ -148,3 +148,39 @@ try apply (sum_bases_ge_OQ []); apply (sum_bases_ge_OQ l1); qed. +lemma sum_bases_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 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. + 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 96cd96e49..d3d63233c 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -15,62 +15,8 @@ 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 le_le_eq: ∀x,y:Q. x ≤ y → y ≤ x → x = y. -axiom q_le_OQ_Qpos: ∀x.OQ ≤ Qpos x. - lemma initial_shift_same_values: ∀l1:q_f.∀init.init < start l1 → same_values l1 @@ -137,25 +83,65 @@ whd in ⊢ (% → ?); simplify in H3; rewrite < q_plus_assoc; rewrite < q_elim_minus; 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;]] + 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 ⊢ (? ? ? (? ? ? (? ? % ? ?))); + simplify in H5 H6 ⊢ (? ? ? (? ? ? (? ? % ? ?))); + +axiom nth_nil: ∀T,n.∀d:T. nth [] d n = d. + +lemma key: + ∀init,input,l1,w1,w2,w. + Qpos w = start l1 - init → + init < start l1 → + start l1 < input → + sum_bases (〈w,OQ〉::bars l1) w1 ≤ ⅆ[input,init] → + ⅆ[input,init] < sum_bases (bars l1) w1 + (start l1-init) → + sum_bases (bars l1) w2 ≤ ⅆ[input,start l1] → + ⅆ[input,start l1] < sum_bases (bars l1) (S w2) → + \snd (nth (bars l1) ▭ w2) = \snd (nth (〈w,OQ〉::bars l1) ▭ w1). +intros 4 (init input l); cases l (st l); +change in match (start (mk_q_f st l)) with st; +change in match (bars (mk_q_f st l)) with l; +elim l; +[1: rewrite > nth_nil; cases w1 in H4; + [1: rewrite > q_d_sym; rewrite > q_d_noabs; [2: + apply (q_le_trans ? st); apply q_lt_to_le; assumption] + do 2 rewrite > q_elim_minus; rewrite > q_plus_assoc; + intro X; lapply (q_lt_canc_plus_r ??? X) as Y; + simplify in Y; cases (?:False); + apply (q_lt_corefl st); apply (q_lt_trans ??? H2); + apply (q_lt_le_trans ??? Y); rewrite > q_plus_sym; rewrite > q_plus_OQ; + apply q_eq_to_le; reflexivity; + |2: intros; simplify; rewrite > nth_nil; reflexivity;] +|2: FACTORIZE w1>0 + + (* interesting case: init < start < input *) + intro; cases H8; clear H8; rewrite > H11; rewrite > H7; clear H11 H7; + simplify in H5 H6 ⊢ (? ? ? (? ? ? (? ? % ? ?))); + elim (\fst w2) in H9 H10; + [1: elim (\fst w1) in H5 H6; + [1: cases (?:False); clear H5 H8 H7; + 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; apply (q_lt_canc_plus_r ?? (Qopp init)); + do 2 rewrite < q_elim_minus; assumption; + |2: + 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: + cases (\fst w1) in H5 H6; intros; [1: + cases (?:False); clear H5 H9 H10; + 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; apply (q_lt_canc_plus_r ?? (Qopp init)); + do 2 rewrite < q_elim_minus; assumption;] + apply eq_f; + cut (sum_bases (bars l1) (\fst w2) < sum_bases (bars l1) (S n));[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] 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 82832c4bc..2073c8a77 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_support.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma @@ -33,6 +33,7 @@ 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. (* order over Q *) axiom qlt : ℚ → ℚ → CProp. @@ -68,6 +69,8 @@ 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 @@ -90,3 +93,19 @@ axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x]. (* integral part *) axiom nat_of_q: ℚ → nat. +(* 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; +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. +