From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 22 Jul 2008 08:34:00 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4895
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b5564e329d48efa6c2ca01da18203def26a70294;p=helm.git

...
---

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 2ca8fc3ce..f50088d8f 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -52,19 +52,78 @@ coercion inject with 0 1 nocomposites.
 axiom devil : False.
         
 definition copy ≝
- λl:list bar.make_list ? (λn.〈nth_base l (n - \len l),〈OQ,OQ〉〉) (\len l).
+ λl:list bar.make_list ? (λn.〈nth_base l (\len l - S n),〈OQ,OQ〉〉) (\len l).
+
+lemma list_elim_with_len:
+  ∀T:Type.∀P: nat → list T → CProp.
+    P O [] → (∀l,a,n.P (\len l) l → P (S n) (a::l)) →
+     ∀l.P (\len l) l.
+intros;elim l; [assumption] simplify; apply H1; apply H2;
+qed.
  
+lemma sorted_near:
+ ∀r,l. sorted r l → ∀i,d. S i < \len l → r (\nth l d i) (\nth l d (S i)).
+ intros 3; elim H; 
+ [1: cases (not_le_Sn_O ? H1);
+ |2: simplify in H1; cases (not_le_Sn_O ? (le_S_S_to_le ?? H1));
+ |3: simplify; cases i in H4; intros; [apply H1]
+     apply H3; apply le_S_S_to_le; apply H4]
+ qed.  
+ 
+lemma sorted_copy:
+  ∀l:list bar.sorted q2_lt l → sorted q2_lt (copy l).
+intros 2; unfold copy; generalize in match (le_n (\len l)); 
+elim (\len l) in ⊢ (?%?→? ? (? ? ? %));
+simplify; [apply (sorted_nil q2_lt);] cases n in H1 H2;
+simplify; intros; [apply (sorted_one q2_lt);]
+apply (sorted_cons q2_lt);
+[2: apply H1; apply lt_to_le; apply H2;
+|1: elim l in H2 H; simplify; [simplify in H2; cases (not_le_Sn_O ? H2)]    
+    simplify in H3; unfold nth_base;
+    unfold canonical_q_lt; unfold q2_trel; unfold q2_lt; simplify;
+    change with (q2_lt (\nth (a::l1) ▭ (\len l1-S n1)) (\nth (a::l1) ▭ (\len l1-n1)));
+    cut (∃w.w = \len l1 - S n1); [2: exists[apply (\len l1 - S n1)] reflexivity]
+    cases Hcut; rewrite < H4; rewrite < (?:S w = \len l1 - n1);
+    [1: apply (sorted_near q2_lt (a::l1) H2); rewrite > H4;
+        simplify; apply le_S_S; elim (\len l1) in H3; simplify;
+        [ cases (not_le_Sn_O ? (le_S_S_to_le ?? H3));
+        | lapply le_S_S_to_le to H5 as H6;
+          lapply le_S_S_to_le to H6 as H7; clear H5 H6;
+          cases H7 in H3; intros; [rewrite < minus_n_n; apply le_S_S; apply le_O_n]
+          simplify in H5; apply le_S_S; apply (trans_le ???? (H5 ?));
+          [2: apply le_S_S; apply le_S_S; assumption;
+          |1: apply (lt_minus_S_n_to_le_minus_n n1 (S m) (S (minus m n1)) ?).
+              apply (not_le_to_lt (S (minus m n1)) (minus (S m) (S n1)) ?).
+              apply (not_le_Sn_n (minus (S m) (S n1))).]]
+    |2: rewrite > H4; lapply le_S_S_to_le to H3 as K;
+        clear H4 Hcut H3 H H1 H2; generalize in match K; clear K;
+        apply (nat_elim2 ???? n1 (\len l1)); simplify; intros;
+        [1: rewrite < minus_n_O; cases n2 in H; [intro; cases (not_le_Sn_O ? H)]
+            intros; cases n3; simplify; reflexivity;
+        |2: cases (not_le_Sn_O ? H);
+        |3: apply H; apply le_S_S_to_le; apply H1;]]]
+qed.
+    
 lemma copy_rebases: 
   ∀l1.rebase_spec_aux l1 [] 〈l1, copy l1〉.
-intros; cases l1; intros 4;
+intros; elim l1; intros 4;
 [1: split; [left; reflexivity]; split; try assumption; unfold; intros;
     unfold same_values; intros; reflexivity;
-|2: rewrite > H2; [2: intro X; destruct X] clear H2 H3;
+|2: rewrite > H3; [2: intro X; destruct X]
     split; [left; reflexivity] split; 
     unfold same_values_simpl; unfold same_values; intros; try reflexivity;
-    try assumption; [4: normalize in p2; destruct p2|2: cases H2; reflexivity;]
-    simplify; clear H1;
-    [1: elim (\len l) in H; simplify; [apply (sorted_one q2_lt);]
+    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; 
+        
+