From 23dbce6cd7d599c10eb7801e91bc8b5164164418 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Jul 2008 12:00:22 +0000 Subject: [PATCH] shift almost done --- .../contribs/dama/dama/models/q_bars.ma | 24 ++--- .../contribs/dama/dama/models/q_function.ma | 88 ++++++++++++++++++- .../contribs/dama/dama/models/q_support.ma | 4 + 3 files changed, 102 insertions(+), 14 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 2b4c8abd0..c67bb501e 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -220,22 +220,26 @@ lemma value_OQ_e: intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1; try assumption; cases H2; cases (?:False); apply (H1 H); qed. + +inductive value_ok_spec (f : q_f) (i : ℚ) : nat × ℚ → Type ≝ + | value_ok : ∀n,q. n ≤ (len (bars f)) → + q = \snd (nth (bars f) ▭ n) → + sum_bases (bars f) n ≤ ⅆ[i,start f] → + ⅆ[i, start f] < sum_bases (bars f) (S n) → value_ok_spec f i 〈n,q〉. lemma value_ok: - ∀f,i. bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) → - And4 - (\fst (\fst (value f i)) ≤ (len (bars f))) - (\snd (\fst (value f i)) = \snd (nth (bars f) ▭ (\fst (\fst (value f i))))) - (sum_bases (bars f) (\fst (\fst (value f i))) ≤ ⅆ[i,start f]) - (ⅆ[i, start f] < sum_bases (bars f) (S (\fst (\fst (value f i))))). -intros; cases (value f i); cases H3; simplify; clear H3; cases H4; + ∀f,i.bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) → + value_ok_spec f i (\fst (value f i)). +intros; cases (value f i); simplify; +cases H3; simplify; clear H3; cases H4; clear H4; [1,2,3: cases (?:False); [1: apply (q_lt_le_incompat ?? H3 H1); |2: apply (q_lt_le_incompat ?? H2 H3); |3: apply (H H3);] -|4: split; cases H7; try assumption;] -qed. - +|4: cases H7; clear H7; cases w in H3 H4 H5 H6 H8; simplify; intros; + constructor 1; assumption;] +qed. + definition same_values ≝ λl1,l2:q_f. ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). 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 bf2eb82d8..3275f86f0 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -15,6 +15,26 @@ include "nat_ordered_set.ma". include "models/q_bars.ma". +lemma key: + ∀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. + lemma initial_shift_same_values: ∀l1:q_f.∀init.init < start l1 → same_values l1 @@ -37,10 +57,70 @@ cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1; rewrite > q_plus_OQ; apply q_eq_to_le; reflexivity;] rewrite > (value_OQ_r ?? K); simplify; symmetry; assumption; |3: simplify in Hi1; destruct Hi1; -|4: - -STOP - +|4: cases (q_cmp input (start l1)); + [2: rewrite > (value_OQ_l ?? H4); + change with (OQ = \snd v1); rewrite > Hv12; + cases H3; clear H3; simplify in H5; cases (\fst v1) in H5;[intros;reflexivity] + simplify; rewrite > q_d_sym; rewrite > q_d_noabs; [2:cases Hi1; apply H5] + rewrite > H2; do 2 rewrite > q_elim_minus;rewrite > q_plus_assoc; + intro X; lapply (q_le_canc_plus_r ??? X) as Y; clear X; + (* OK *) + |1,3: cases Hi1; clear Hi1; cases H3; clear H3; + simplify in H5 H6 H8 H9 H7:(? ? (? % %)) ⊢ (? ? ? (? ? ? %)); + generalize in match (refl_eq ? (bars l1):bars l1 = bars l1); + generalize in ⊢ (???% → ?); intro X; cases X; clear X; intro Hb; + [1,3: rewrite > (value_OQ_e ?? Hb); rewrite > Hv12; rewrite > Hb in Hv11 ⊢ %; + simplify in Hv11 ⊢ %; cases (\fst v1) in Hv11; [1,3:intros; reflexivity] + cases n; [1,3: intros; reflexivity] intro X; cases (not_le_Sn_O ? (le_S_S_to_le ?? X)); + |2,4: cases (value_ok l1 input); + [1,5: rewrite > Hv12; rewrite > Hb; clear Hv12; simplify; + rewrite > H10; rewrite > Hb; + cut (O < \fst v1);[2,4: cases (\fst v1) in H9; intros; [2,4: autobatch] + cases (?:False); generalize in match H9; + rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption] + rewrite > H2; simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; + repeat rewrite > q_elim_minus; + intro X; lapply (q_lt_canc_plus_r ??? X) as Y; + apply (q_lt_le_incompat ?? Y); + [apply q_eq_to_le;symmetry|apply q_lt_to_le] assumption;] + cases (\fst v1) in H8 H9 Hcut; [1,3:intros (_ _ X); cases (not_le_Sn_O ? X)] + intros; clear H13; simplify; + rewrite > (key n n1 (b::l)); [1,4: reflexivity] rewrite < Hb; + [2,4: simplify in H8; apply (q_le_lt_trans ??? (q_le_plus_r ??? H8)); + apply (q_le_lt_trans ???? H12); rewrite > H2; + rewrite > q_d_sym; rewrite > q_d_noabs; [2,4: assumption] + rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; + rewrite > q_elim_opp; repeat rewrite > q_elim_minus; + rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); + rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? (? % ?) ?); + rewrite > (q_plus_sym ? init); do 2 rewrite < q_elim_minus; + rewrite > q_plus_minus; rewrite > q_plus_OQ; + rewrite > q_d_sym; rewrite > q_d_noabs; + [2,4: [apply q_eq_to_le; symmetry|apply q_lt_to_le] assumption] + apply q_eq_to_le; reflexivity; + |*: apply (q_le_lt_trans ??? H11); + rewrite > q_d_sym; rewrite > q_d_noabs; + [2,4: [apply q_eq_to_le; symmetry|apply q_lt_to_le] assumption] + generalize in match H9; rewrite > q_d_sym; rewrite > q_d_noabs; + [2,4: assumption] + rewrite > H2; intro X; + lapply (q_lt_inj_plus_r ?? (Qopp (start l1-init)) X) as Y; clear X; + rewrite < q_plus_assoc in Y; repeat rewrite < q_elim_minus in Y; + rewrite > q_plus_minus in Y; rewrite > q_plus_OQ in Y; + apply (q_le_lt_trans ???? Y); + rewrite > (q_elim_minus (start l1) init); rewrite > q_minus_distrib; + rewrite > q_elim_opp; repeat rewrite > q_elim_minus; + rewrite < q_plus_assoc; rewrite > (q_plus_sym ? init); + rewrite > q_plus_assoc;rewrite < q_plus_assoc in ⊢ (? ? (? % ?)); + rewrite > (q_plus_sym ? init); rewrite < (q_elim_minus init); + rewrite > q_plus_minus; rewrite > q_plus_OQ; + apply q_eq_to_le; reflexivity;] + |2,6: rewrite > Hb; intro W; destruct W; + |3,7: [apply q_eq_to_le;symmetry|apply q_lt_to_le] assumption; + |4,8: apply (q_lt_le_trans ??? H7); rewrite > H2; + rewrite > q_plus_sym; rewrite < q_plus_assoc; + rewrite > q_plus_sym; apply q_le_inj_plus_r; + apply q_le_minus; apply q_eq_to_le; reflexivity;]]] 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 index 9d73f7ab9..b948e61b5 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_support.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma @@ -52,6 +52,10 @@ 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. 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. -- 2.39.2