shift almost done

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 2b4c8abd05f15136055f606a025b0fb26e01d8de..c67bb501e8ab6e7d170311dee42f30ee434f630b 100644 (file)
--- 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 bf2eb82d8f210ffdb8e9c3e362bb5fa7da2e6278..3275f86f04134d6c1743ca397651ae1457aa923f 100644 (file)
--- 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 9d73f7ab9b209fdfa887c3aed98764d3cd737265..b948e61b5d8dc1e936e499e82de27bbb1a26b44e 100644 (file)
--- 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.