...

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 f50088d8f632ca6fed022ea072f628f3a58e67af..a38cf6e4cda648377be8ea314956b673a2f2becd 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -103,7 +103,47 @@ apply (sorted_cons q2_lt);
         |2: cases (not_le_Sn_O ? H);
         |3: apply H; apply le_S_S_to_le; apply H1;]]]
 qed.
+
+lemma make_list_ext: ∀T,f1,f2,n. (∀x.x<n → f1 x = f2 x) → make_list T f1 n = make_list T f2 n.
+intros 4;elim n; [reflexivity] simplify; rewrite > H1; [2: apply le_n]
+apply eq_f; apply H; intros; apply H1; apply (trans_le ??? H2); apply le_S; apply le_n;
+qed.
+    
+lemma len_copy: ∀l. \len l = \len (copy l).
+intro; elim l; [reflexivity] simplify; rewrite > H; clear H;
+apply eq_f; elim (\len (copy l1)) in ⊢ (??%(??(???%))); [reflexivity] simplify;
+rewrite > H in ⊢ (??%?); reflexivity;
+qed. 
+
+lemma same_bases_cons: ∀a,b,l1,l2.
+  same_bases l1 l2 → \fst a = \fst b → same_bases (a::l1) (b::l2).
+intros; intro; cases i; simplify; [assumption;] apply (H n);
+qed.
+
+lemma minus_lt : ∀i,j. i < j → j - i = S (j - S i). 
+intros 2;
+apply (nat_elim2 ???? i j); simplify; intros;
+[1: cases n in H; intros; rewrite < minus_n_O; [cases (not_le_Sn_O ? H);]
+    simplify; rewrite < minus_n_O; reflexivity;
+|2: cases (not_le_Sn_O ? H);
+|3: apply H; apply le_S_S_to_le; assumption;]
+qed.
     
+lemma copy_same_bases: ∀l. same_bases l (copy l).
+intro; unfold copy; elim l using list_elim_with_len; [1: intro;reflexivity]
+simplify; rewrite < minus_n_n;
+simplify in ⊢ (? ? (? ? (? ? ? % ?) ?));
+apply same_bases_cons; [2: reflexivity]
+cases l1 in H; [intros 2; reflexivity]
+simplify in ⊢ (? ? (? ? (λ_:?.? ? ? (? ? %) ?) ?)→?);
+simplify in ⊢ (?→? ? (? ? (λ_:?.? ? ? (? ? (? % ?)) ?) ?));
+intro; rewrite > (make_list_ext ?? (λn:nat.〈nth_base (b::l2) (\len l2-n),〈OQ,OQ〉〉));[assumption]
+intro; elim x; [simplify; rewrite < minus_n_O; reflexivity]
+simplify in ⊢ (? ? (? ? ? (? ? %) ?) ?);
+simplify in H2:(? ? %); rewrite > minus_lt; [reflexivity] apply le_S_S_to_le;
+assumption;
+qed.
+
 lemma copy_rebases: 
   ∀l1.rebase_spec_aux l1 [] 〈l1, copy l1〉.
 intros; elim l1; intros 4;
@@ -114,20 +154,22 @@ intros; elim l1; intros 4;
     unfold same_values_simpl; unfold same_values; intros; try reflexivity;
     try assumption; [4: normalize in p2; destruct p2|2: cases H5; reflexivity;]
     [1: apply (sorted_copy ? H1);
-    |2: cases H; try assumption;[2:apply (sorted_tail q2_lt ?? H1);
-        |3: intro; cases l in H5 H3; [intros (_ X); cases X; reflexivity]
-            intros; rewrite < H3; simplify; [2: intro X; destruct X]
-            reflexivity]
-        cases H8; clear H11 H10 H8 H7 H6 H5 H4 H3; simplify;
-        simplify in H9;sq elim l in H9; [rewrite < minus_n_n; intro; simplify;
-          elim i; [reflexivity] simplify; reflexivity;]    
-        simplify; apply H3; 
-        
-        
-        
-        
-    
-        
+    |2: apply (copy_same_bases (a::l));]]
+qed.
+               
+lemma copy_rebases_r: 
+  ∀l1.rebase_spec_aux [] l1 〈copy l1, l1〉.
+intros; elim l1; intros 4;
+[1: split; [left; reflexivity]; split; try assumption; unfold; intros;
+    unfold same_values; intros; reflexivity;
+|2: rewrite > H4; [2: intro X; destruct X]
+    split; [right; simplify; rewrite < minus_n_n; reflexivity] split; 
+    unfold same_values_simpl; unfold same_values; intros; try reflexivity;
+    try assumption; [4: normalize in p2; destruct p2|2: cases H5; reflexivity;]
+    [1: apply (sorted_copy ? H2);
+    |2: intro; symmetry; apply (copy_same_bases (a::l));]]
+qed.
+               
 definition rebase: ∀l1,l2:q_f.∃p:q_f × q_f.rebase_spec l1 l2 p.
 intros 2 (f1 f2); cases f1 (b1 Hs1 Hb1 He1); cases f2 (b2 Hs2 Hb2 He2); clear f1 f2;
 alias symbol "plus" = "natural plus".
@@ -163,9 +205,9 @@ match n with
              let rest ≝ base1 - base2 in
              let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
              〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉]]]]
-in aux : ∀l1,l2,m.∃z.m = \len l1 + \len l2 → rebase_spec_aux l1 l2 z);
+in aux : ∀l1,l2,m.∃z.\len l1 + \len l2 ≤ m → rebase_spec_aux l1 l2 z);
 [7: clearbody aux; cases (aux b1 b2 (\len b1 + \len b2)) (w Hw); clear aux;
-    cases (Hw (refl_eq ??) Hs1 Hs2 (λ_.He1) (λ_.He2)); clear Hw; cases H1; cases H2; cases H3; clear H3 H1 H2;
+    cases (Hw (le_n ?) Hs1 Hs2 (λ_.He1) (λ_.He2)); clear Hw; cases H1; cases H2; cases H3; clear H3 H1 H2;
     exists [constructor 1;constructor 1;[apply (\fst w)|5:apply (\snd w)]] try assumption;
     [1,3: apply hide; cases H (X X); try rewrite < (H8 O); try rewrite < X; assumption
     |2,4: apply hide;[apply H6|apply H7]intro X;[rewrite > X in Hb1|rewrite > X in Hb2]
@@ -174,11 +216,30 @@ in aux : ∀l1,l2,m.∃z.m = \len l1 + \len l2 → rebase_spec_aux l1 l2 z);
     simplify in match (\snd 〈?,?〉); simplify in match (\fst 〈?,?〉);
     split; [assumption; |apply H9;|apply H10]
 |6: intro ABS; unfold; intros 4; clear H1 H2;
-    cases l in ABS H3; intros 1; [2: simplify in H1; destruct H1]
-    cases l1 in H4 H1; intros; [2: simplify in H2; destruct H2]
-    split; [left;reflexivity|split; apply (sorted_nil q2_lt);|split; assumption;]
+    cases l in ABS H3; intros 1; [2: simplify in H1; cases (not_le_Sn_O ? H1)]
+    cases l1 in H4 H1; intros; [2: simplify in H2; cases (not_le_Sn_O ? H2)]
+    split; [ left; reflexivity|split; apply (sorted_nil q2_lt);|split; assumption;]
     split; unfold; intros; unfold same_values; intros; reflexivity;
-|5: unfold rebase_spec_aux; intros; cases l1 in H2 H4 H6; intros; [ simplify in H2; destruct H2;]
+|5: intros; apply copy_rebases_r;
+|4: intros; rewrite < H1; apply copy_rebases;
+|3: cut (\fst b = \fst b3) as K; [2: apply q_le_to_le_to_eq; assumption] clear H6 H5 H4 H3;
+    intros; cases (aux l2 l3 n1); intros 4; simplify in match (\fst ≪w,H≫);
+    simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉);
+    cases H4; 
+      [2: apply le_S_S_to_le; apply (trans_le ???? H3); simplify;
+          rewrite < plus_n_Sm; apply le_S; apply le_n;
+      |3,4: apply (sorted_tail q2_lt); [2: apply H5|4:apply H6]
+      |5: intro; cases l2 in H7 H9; intros; [cases H9; reflexivity]
+          simplify in H7 ⊢ %; apply H7; intro; destruct H10;
+      |6: intro; cases l3 in H8 H9; intros; [cases H9; reflexivity]
+          simplify in H8 ⊢ %; apply H8; intro; destruct H10;]
+    clear aux; split; 
+    [1: left; reflexivity;
+    |2: cases H10;  
+
+    
+     
+ unfold rebase_spec_aux; intros; cases l1 in H2 H4 H6; intros; [ simplify in H2; destruct H2;]
     lapply H6 as H7; [2: intro X; destruct X] clear H6 H5;
     rewrite > H7; split; [right; simplify;
     

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 70b3e6ade4b21544c6385be1d58b313167f50ec8..4f27f398a42d9963a35f31c08e903666ec403d73 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -48,6 +48,8 @@ inductive q_le_elimination (a,b:ℚ) : CProp ≝
 
 axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
 
+axiom q_le_to_le_to_eq : ∀x,y. x ≤ y → y ≤ x → x = y.
+
 axiom q_le_plus_l: ∀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_l: ∀a,b,c:ℚ. a < c - b → a + b < c.