some more work

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 21e51808a10189754f4e0e7e80736a562c9168df..5d642228d470c5751c172323968bd098a6b23f03 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -43,6 +43,7 @@ definition qle ≝ λa,b:ℚ.a = b ∨ a < b.
 interpretation "Q less or equal than" 'leq x y = (qle x y).
 
 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.
 
@@ -194,7 +195,16 @@ 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. 
+  ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
+axiom q_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_d_noabs: ∀x,y. x ≤ y → ⅆ[x,y] = y - x.
+axiom q_d_sym:  ∀x,y. ⅆ[x,y] = ⅆ[y,x].
+axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
+axiom q_plus_minus: ∀x.Qpos x + Qneg 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. 
 
 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
 intro; cases x; intros; [2:exists [apply r] reflexivity]
@@ -247,11 +257,46 @@ whd in ⊢ (% → ?); simplify in H3;
         rewrite > H7; clear H7; rewrite > (?:\fst w1 = O); [reflexivity]
         symmetry; apply le_n_O_to_eq;
         rewrite > (sum_bases_O (mk_q_f init (〈w,OQ〉::bars l1)) (\fst w1)); [apply le_n]   
-        clear H6 w2;
-        simplify in H5:(? ? (? ? %));  
+        clear H6 w2; simplify in H5:(? ? (? ? %));  
         destruct H3; rewrite > q_d_x_x in H5; assumption;]
-|2: intros;
-  
+|2: intros; cases (value l1 input); simplify in ⊢ (? ? (? ? ? %) ?);
+    cases (q_cmp input (start l1)) in H5; whd in ⊢ (% → ?);
+    [1: cases (?:False); clear w2 H4 w1 H2 w H1; 
+        apply (q_lt_antisym init (start l1)); [assumption] rewrite < H5; assumption
+    |2: intros; rewrite > H6; clear H6; rewrite > H4; reflexivity;
+    |3: cases (?:False); apply (q_lt_antisym input (start l1)); [2: assumption]
+        apply (q_lt_trans ??? H3 H);]
+|3: intro; cases H4; clear H4;   
+    cases (value l1 input); simplify; cases (q_cmp input (start l1)) in H4; whd in ⊢ (% → ?);
+    [1: 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;]
+        cut (\fst w2 = O); [2: clear H10;
+          symmetry; apply le_n_O_to_eq; rewrite > (sum_bases_O l1 (\fst w2)); [apply le_n]
+          apply (q_le_trans ??? H9); rewrite < H4; rewrite > q_d_x_x; 
+          left; reflexivity;]
+        rewrite > Hcut; clear Hcut H10 H9; simplify in H5 H6;
+        cut (ⅆ[input,init] = Qpos w) as E; [2:
+          rewrite > H2; rewrite < H4; rewrite > q_d_sym; 
+          rewrite > q_d_noabs; [reflexivity] right; assumption;]
+        cases (\fst w1) in H5 H6; intros;
+        [1: cases (?:False); clear H5; simplify in H6;
+            apply (q_lt_corefl ⅆ[input,init]);
+            rewrite > E in ⊢ (??%); rewrite < q_plus_OQ in ⊢ (??%);
+            rewrite > q_plus_sym; assumption;
+        |2: cases n in H5 H6; [intros; reflexivity] intros;
+            cases (?:False); clear H6; cases (bars l1) in H5; simplify; intros;
+            [apply (q_pos_OQ one);|apply (q_pos_OQ (\fst b));] 
+            apply (q_le_S ??? (sum_bases_ge_OQ (mk_q_f init ?) n1));[apply [];|3:apply l]
+            simplify in ⊢ (? (? (? % ?) ?) ?); rewrite < (q_plus_minus w);
+            apply q_le_minus_r; rewrite < q_minus_r; 
+            rewrite < E in ⊢ (??%); assumption;]
+    |2: intros; rewrite > H8; rewrite > H7; clear H8 H7;
+        simplify in H5 H6 ⊢ %;
+        simplify in H5:(? ? (? ? %));
+        
+            
+        
 alias symbol "pi2" = "pair pi2".
 alias symbol "pi1" = "pair pi1".
 definition rebase_spec ≝