...

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 2186890f0cf29b007e36fd04eb82380637633e49..f75bed7bebe48b7f736ffe18f5324439493dace8 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -257,15 +257,14 @@ cases H3; simplify; clear H3; cases H4; clear H4;
   |3: apply (H H3);]
 |4: cases H7; clear H7; cases w in H3 H4 H5 H6 H8; simplify; intros;
     constructor 1; assumption;]
-qed.   
+qed.
 
 definition same_values ≝
   λl1,l2:q_f.
    ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). 
 
 definition same_bases ≝ 
-  λl1,l2:q_f.
-    (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)).
+  λl1,l2:list bar. (∀i.\fst (nth l1 ▭ i) = \fst (nth l2 ▭ i)).
 
 alias symbol "lt" = "Q less than".
 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.

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 e2187b51014799aed94ac412bef1ac57f24056d9..b1ff639e44b959bd6a2a482c001df38d552316f9 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -20,16 +20,15 @@ alias symbol "pi1" = "pair pi1".
 definition rebase_spec ≝ 
  ∀l1,l2:q_f.∃p:q_f × q_f.
    And4
-    (*len (bars (\fst p)) = len (bars (\snd p))*)
     (start (\fst p) = start (\snd p))
-    (same_bases (\fst p) (\snd p))
+    (same_bases (bars (\fst p)) (bars (\snd p)))
     (same_values l1 (\fst p)) 
     (same_values l2 (\snd p)).
 
 definition rebase_spec_simpl ≝ 
  λstart.λl1,l2:list bar.λp:(list bar) × (list bar).
    And3
-    (same_bases (mk_q_f start (\fst p)) (mk_q_f start (\snd p)))
+    (same_bases (\fst p) (\snd p))
     (same_values (mk_q_f start l1) (mk_q_f start (\fst p))) 
     (same_values (mk_q_f start l2) (mk_q_f start (\snd p))).
 
@@ -42,6 +41,8 @@ definition eject ≝
 coercion eject.
 definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h.
 coercion inject with 0 1 nocomposites.
+
+axiom devil : False.
         
 definition rebase: rebase_spec.
 intros 2 (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2;
@@ -86,7 +87,7 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec;
         [1,2: assumption;
         |3: intro; apply (H3 input);
         |4: intro; rewrite > H in H4; 
-            rewrite > (H4 input); reflexivity;]
+            rewrite > (H4 input) in ⊢ (? ? % ?); reflexivity;]
     |2: letin l2' ≝ (〈\fst (unpos (s2-s1) ?),OQ〉::l2);[
           apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
           assumption]
@@ -96,8 +97,9 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec;
         [1: reflexivity
         |2: assumption;
         |3: assumption;
-        |4: intro; rewrite > (initial_shift_same_values (mk_q_f s2 l2) s1 H input);
-            rewrite < (H4 input); reflexivity;]
+        |4: intro; 
+            rewrite > (initial_shift_same_values (mk_q_f s2 l2) s1 H input) in ⊢ (? ? % ?);
+            rewrite < (H4 input)in ⊢ (? ? ? %); reflexivity;]
     |3: letin l1' ≝ (〈\fst (unpos (s1-s2) ?),OQ〉::l1);[
           apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
           assumption]
@@ -107,8 +109,9 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec;
         [1: reflexivity
         |2: assumption;
         |4: assumption;
-        |3: intro; rewrite > (initial_shift_same_values (mk_q_f s1 l1) s2 H input);
-            rewrite < (H3 input); reflexivity;]]
+        |3: intro; simplify in ⊢ (? ? ? (? ? ? (? ? ? (? % ?))));
+            rewrite > (initial_shift_same_values (mk_q_f s1 l1) s2 H input) in ⊢ (? ? % ?);
+            rewrite < (H3 input) in ⊢ (? ? ? %); reflexivity;]]
 |1,2: unfold rest; apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ;
       assumption;        
 |8: intros; cases (?:False); apply (not_le_Sn_O ? H1);
@@ -124,7 +127,7 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec;
         cases (H4 s K); clear K H4; intro input; cases input; [reflexivity]
         simplify; apply H7; 
     |2: simplify in ⊢ (? ? %); cases (H4 s K); clear H4 K H5 spec;
-        intro; 
+        intro;
         (* input < s + b1 || input >= s + b1 *)
     |3: simplify in ⊢ (? ? %);]   
 |4: intros; generalize in match (unpos ??); intro X; cases X; clear X;
@@ -132,4 +135,59 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec;
 |5: intros; (* triviale, caso in cui non fa nulla *)
 |6,7: (* casi base in cui allunga la lista più corta *) 
 ]
+elim devil;
 qed.
+
+include "Q/q/qtimes.ma".
+
+let rec area (l:list bar) on l ≝
+  match l with 
+  [ nil ⇒ OQ
+  | cons he tl ⇒ area tl + Qpos (\fst he) * ⅆ[OQ,\snd he]].
+
+alias symbol "pi1" = "exT \fst".
+alias symbol "minus" = "Q minus".
+alias symbol "exists" = "CProp exists".
+definition minus_spec_bar ≝
+ λf,g,h:list bar.
+   same_bases f g → len f = len g →
+     ∀s,i:ℚ. \snd (\fst (value (mk_q_f s h) i)) = 
+       \snd (\fst (value (mk_q_f s f) i)) - \snd (\fst (value (mk_q_f s g) i)). 
+
+definition minus_spec ≝
+ λf,g:q_f.
+   ∃h:q_f. 
+     ∀i:ℚ. \snd (\fst (value h i)) = 
+       \snd (\fst (value f i)) - \snd (\fst (value g i)). 
+
+definition eject_bar : ∀P:list bar → CProp.(∃l:list bar.P l) → list bar ≝
+ λP.λp.match p with [ex_introT x _ ⇒ x].
+definition inject_bar ≝ ex_introT (list bar).
+
+coercion inject_bar with 0 1 nocomposites.
+coercion eject_bar with 0 0 nocomposites.
+
+lemma minus_q_f : ∀f,g. minus_spec f g.
+intros;
+letin aux ≝ (
+  let rec aux (l1, l2 : list bar) on l1 ≝
+    match l1 with
+    [ nil ⇒ []
+    | cons he1 tl1 ⇒
+        match l2 with
+        [ nil ⇒ []
+        | cons he2 tl2 ⇒ 〈\fst he1, \snd he1 - \snd he2〉 :: aux tl1 tl2]]
+  in aux : ∀l1,l2 : list bar.∃h.minus_spec_bar l1 l2 h);
+[2: intros 4; simplify in H3; destruct H3;
+|3: intros 4; simplify in H3; cases l1 in H2; [2: intro X; simplify in X; destruct X]    
+    intros; rewrite > (value_OQ_e (mk_q_f s []) i); [2: reflexivity]
+    rewrite > q_elim_minus; rewrite > q_plus_OQ; reflexivity;
+|1: cases (aux l2 l3); unfold in H2; intros 4;
+    simplify in ⊢ (? ? (? ? ? (? ? ? (? % ?))) ?);
+    cases (q_cmp i (s + Qpos (\fst b)));
+    
+
+
+definition excess ≝ 
+  λf,g.∃i.\snd (\fst (value f i)) < \snd (\fst (value g i)).
+  

diff --git a/helm/software/matita/contribs/dama/dama/models/q_shift.ma b/helm/software/matita/contribs/dama/dama/models/q_shift.ma
index f247fb11d8a9c74b6b8b436da031563e258a2023..a630666595aaee63616e187c98b7bedb54917980 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_shift.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_shift.ma
@@ -103,3 +103,4 @@ cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1;
       |1: apply solution; apply (q_eq_to_le ?? (sym_eq ??? H4));
       |3: apply solution; apply (q_lt_to_le ?? H4);]
 qed.        
+