X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_copy.ma;h=de7384077ee93d07a1dfcbbdb12974b29a388dab;hb=6d27950e804ea499909ae0fabceea99f35d118e9;hp=78e4ea821526dd6f41ee4a972599c4c216cc7d8d;hpb=31126ffda75cba3fbc6572d86e910c10940da46c;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/q_copy.ma b/helm/software/matita/contribs/dama/dama/models/q_copy.ma
index 78e4ea821..de7384077 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_copy.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_copy.ma
@@ -24,76 +24,43 @@ apply (nat_elim2 ???? i j); simplify; intros;
 |3: apply H; apply le_S_S_to_le; assumption;]
 qed.
 
-definition copy ≝
- λl:list bar.make_list ? (λn.〈nth_base l (\len l - S n),〈OQ,OQ〉〉) (\len l).
+alias symbol "lt" = "bar lt".
+lemma inversion_sorted:
+  ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []).
+intros 2; elim l; [right;reflexivity] left; inversion H1; intros;
+[1,2:destruct H2| destruct H5; assumption]
+qed.
+
+lemma inversion_sorted2:
+  ∀a,b,l. sorted q2_lt (a::b::l) → a < b.
+intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption; 
+qed.
+
+let rec copy (l : list bar) on l : list bar ≝
+  match l with
+  [ nil ⇒ []
+  | cons x tl ⇒ 〈\fst x, 〈OQ,OQ〉〉 :: copy tl].
 
 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;]]]
+intro l; elim l; [apply (sorted_nil q2_lt)] simplify;
+cases l1 in H H1; simplify; intros; [apply (sorted_one q2_lt)]
+apply (sorted_cons q2_lt); [2: apply H; apply (sorted_tail q2_lt ?? H1);]
+apply (inversion_sorted2 ??? H1);
 qed.
 
 lemma len_copy: ∀l. \len (copy l) = \len l. 
-intro; unfold copy; apply len_mk_list;
+intro; elim l; [reflexivity] simplify; apply eq_f; 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 > (mk_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 rewrite_ext_nth_height : ∀n,m,f,f1,g,g1. (∀t.g t = g1 t) →
-nth_height (\mk_list (λn.〈f n,g n〉) m) n = nth_height (\mk_list (λn.〈f1 n,g1 n〉) m) n.
-intros; generalize in match n; clear n; elim m; [reflexivity] simplify;
-cases n1; [simplify;apply H;] simplify; apply (H1 n2);
+intros; elim l; [intro; reflexivity] intro; simplify; cases i; [reflexivity]
+simplify; apply (H n);
 qed.
 
 lemma copy_OQ : ∀l,n.nth_height (copy l) n = 〈OQ,OQ〉.
-intro; elim l; [cases n; [reflexivity] simplify; rewrite > nth_nil; reflexivity]
-cases n; simplify [reflexivity]
-change with (nth_height (\mk_list (λn:ℕ.〈nth_base (a::l1) (\len l1-n),〈OQ,OQ〉〉) (\len l1)) n1 = 〈OQ,OQ〉);
-rewrite > (rewrite_ext_nth_height ??? (λ_.OQ) ? (λ_.〈OQ,OQ〉)); [2: intros; reflexivity]
-generalize in match n1;
-elim (\len l1); simplify; unfold nth_height; [rewrite > nth_nil; reflexivity]
-cases n3; simplify; [reflexivity] apply (H1 n4);
+intro; elim l; [elim n;[reflexivity] simplify; assumption]
+simplify; cases n; [reflexivity] simplify; apply (H n1);
 qed.
 
 lemma prepend_sorted_with_same_head:
@@ -118,17 +85,6 @@ try assumption; intros; unfold nth_base in H2; whd in H4;
 |2: cases (H3 H4);]
 qed.
        
-alias symbol "lt" = "bar lt".
-lemma inversion_sorted:
-  ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []).
-intros 2; elim l; [right;reflexivity] left; inversion H1; intros;
-[1,2:destruct H2| destruct H5; assumption]
-qed.
-
-lemma inversion_sorted2:
-  ∀a,b,l. sorted q2_lt (a::b::l) → a < b.
-intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption; 
-qed.
 
 lemma sort_q2lt_same_base:
   ∀b,h1,h2,l. sorted q2_lt (〈b,h1〉::l) → sorted q2_lt (〈b,h2〉::l).
@@ -137,3 +93,54 @@ lapply (sorted_tail q2_lt ?? H) as K; clear H; cases l in H1 K; simplify; intros
 [apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H]
 qed.
 
+lemma value_head : ∀a,l,i.Qpos i ≤ \fst a → value_simple (a::l) i = \snd a.
+intros; unfold value_simple; unfold match_domain; cases (cases_find bar (match_pred i) (a::l) ▭);
+[1: cases i1 in H2 H3 H4; intros; [reflexivity] lapply (H4 O) as K; [2: apply le_S_S; apply le_O_n;]
+    simplify in K; unfold match_pred in K; cases (q_cmp (Qpos i) (\fst a)) in K;
+    simplify; intros; [destruct H6] lapply (q_le_lt_trans ??? H H5) as K; cases (q_lt_corefl ? K); 
+|2: cases (?:False); lapply (H3 0); [2: simplify; apply le_S_S; apply le_O_n;]
+    unfold match_pred in Hletin; simplify in Hletin; cases (q_cmp (Qpos i) (\fst a)) in Hletin;
+    simplify; intros; [destruct H5] lapply (q_le_lt_trans ??? H H4); apply (q_lt_corefl ? Hletin);]
+qed.
+
+lemma value_unit : ∀x,i. value_simple [x] i = \snd x.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) [x] ▭);
+[1: cases i1 in H; intros; [reflexivity] simplify in H;
+    cases (not_le_Sn_O ? (le_S_S_to_le ?? H));
+|2: simplify in H; destruct H; reflexivity;]
+qed.
+
+lemma value_tail : 
+  ∀a,b,l,i.\fst a < Qpos i → \fst b ≤ Qpos i → value_simple (a::b::l) i = value_simple (b::l) i.
+intros; unfold value_simple; unfold match_domain;
+cases (cases_find bar (match_pred i) (a::b::l) ▭);
+[1: cases i1 in H3 H2 H4 H5; intros 1; simplify in ⊢ (? ? (? ? %) ?→?); unfold in ⊢ (? ? % ?→?); intros;
+    [1: cases (?:False); cases (q_cmp (Qpos i) (\fst a)) in H3; simplify; intros;[2: destruct H6]
+        apply (q_lt_corefl ? (q_lt_le_trans ??? H H3));
+    |2:         
+
+normalize in ⊢ (? ? % ?→?); simplify;
+[1: rewrite > (value_head);
+ 
+lemma value_copy : 
+  ∀l,i.rewrite > (value_u
+  value_simple (copy l) i = 〈OQ,OQ〉.
+intros; elim l;
+[1: reflexivity;
+|2: cases l1 in H; intros; simplify in ⊢ (? ? (? % ?) ?);
+    [1: rewrite > (value_unit); reflexivity;
+    |2: cases (q_cmp (\fst b) (Qpos i));  
+ 
+ change with (\fst ▭ = \lamsimplify in ⊢ (? ? (? % ?) ?); unfold value_simple; unfold match_domain; 
+    cases (cases_find bar (match_pred i) [〈\fst x,〈OQ,OQ〉〉] ▭);
+    [1: simplify in H1:(??%%);
+
+ unfold match_pred;
+    rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity;
+|2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?);
+    cases (q_cmp (Qpos i)  (\fst b));
+    [2: rewrite > (value_tail ??? H2 H3 ? H4 H1); apply H;
+    |1: rewrite > (value_head ??? H2 H3 ? H4 H1); reflexivity]]
+qed. 
+    
\ No newline at end of file