X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_bars.ma;h=2cad9ca2add1adbdb9efa018723ee99809c4b99f;hb=a0c0e92cee3ed99995e12b02f18e30f018d946ea;hp=79cc540a87fa2af3346e7f377238adc8c2e9ca94;hpb=99feea74c16b4801a2b1596d5e48e27224ffbfaa;p=helm.git

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 79cc540a8..2cad9ca2a 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat_ordered_set.ma".
+include "dama/nat_ordered_set.ma".
 include "models/q_support.ma".
 include "models/list_support.ma". 
 include "logic/cprop_connectives.ma". 
@@ -31,7 +31,7 @@ interpretation "lq2" 'lq2 = (list bar).
 
 definition q2_lt := mk_rel bar (λx,y:bar.\fst x < \fst y).
 
-interpretation "bar lt" 'lt x y = (rel_op _ q2_lt x y).
+interpretation "bar lt" 'lt x y = (rel_op ? q2_lt x y).
 
 lemma q2_trans : ∀a,b,c:bar. a < b → b < c → a < c.
 intros 3; cases a; cases b; cases c; unfold q2_lt; simplify; intros;
@@ -46,7 +46,7 @@ definition canonical_q_lt : rel bar → trans_rel ≝ λx:rel bar.q2_trel.
 
 coercion canonical_q_lt with nocomposites.
 
-interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel (canonical_q_lt _) x y).
+interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel (canonical_q_lt ?) x y).
 
 definition nth_base ≝ λf,n. \fst (\nth f ▭ n).
 definition nth_height ≝ λf,n. \snd (\nth f ▭ n).
@@ -87,6 +87,15 @@ coinductive value_spec (f : list bar) (i : ℚ) : ℚ × ℚ → CProp ≝
     nth_height f j = q →  nth_base f j < i → j < \len f →
     (∀n.n<j → nth_base f n < i) →
     (∀n.j < n → n < \len f → i ≤ nth_base f n) → value_spec f i q. 
+
+definition match_pred ≝
+ λi.λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false].
+
+definition match_domain ≝
+  λf: list bar.λi:ratio. pred (find ? (match_pred i) f ▭).
+   
+definition value_simple ≝
+  λf: list bar.λi:ratio. nth_height f (match_domain f i).
          
 alias symbol "lt" (instance 5) = "Q less than".
 alias symbol "lt" (instance 6) = "natural 'less than'".
@@ -94,28 +103,26 @@ definition value_lemma :
   ∀f:list bar.sorted q2_lt f → O < length bar f → 
   ∀i:ratio.nth_base f O  < Qpos i → ∃p:ℚ×ℚ.value_spec f (Qpos i) p.
 intros (f bars_sorted_f len_bases_gt_O_f i bars_begin_OQ_f);
-letin P ≝ 
-  (λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false]);
-exists [apply (nth_height f (pred (find ? P f ▭)));]
-apply (value_of ?? (pred (find ? P f ▭)));
+exists [apply (value_simple f i);]
+apply (value_of ?? (match_domain f i));
 [1: reflexivity
-|2: cases (cases_find bar P f ▭);
+|2: unfold match_domain; cases (cases_find bar (match_pred i) f ▭);
     [1: cases i1 in H H1 H2 H3; simplify; intros;
         [1: generalize in match (bars_begin_OQ_f); 
             cases (len_gt_non_empty ?? (len_bases_gt_O_f)); simplify; intros;
             assumption;
         |2: cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H3;
-            intros; lapply (H3 n (le_n ?)) as K; unfold P in K;
+            intros; lapply (H3 n (le_n ?)) as K; unfold match_pred in K;
             cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ n))) in K;
             simplify; intros; [destruct H5] assumption] 
     |2: destruct H; cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H2;
         simplify; intros; lapply (H (\len l) (le_n ?)) as K; clear H;
-        unfold P in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
+        unfold match_pred in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
         simplify; intros; [destruct H2] assumption;]     
-|5: intro; cases (cases_find bar P f ▭); intros;
+|5: intro; unfold match_domain; cases (cases_find bar (match_pred i) f ▭); intros;
     [1: generalize in match (bars_sorted_f); 
         cases (list_break ??? H) in H1; rewrite > H6;
-        rewrite < H1; simplify; rewrite > nth_len; unfold P; 
+        rewrite < H1; simplify; rewrite > nth_len; unfold match_pred; 
         cases (q_cmp (Qpos i) (\fst x)); simplify; 
         intros (X Hs); [2: destruct X] clear X;
         cases (sorted_pivot q2_lt ??? ▭ Hs);
@@ -129,7 +136,7 @@ apply (value_of ?? (pred (find ? P f ▭)));
             repeat rewrite < plus_n_Sm; rewrite < plus_n_O; simplify;
             rewrite > sym_plus; rewrite < minus_plus_m_m; reflexivity;]
           rewrite > len_append; rewrite > H1; simplify; rewrite < plus_n_SO;
-          apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H P;
+          apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H;
           elim (\len f) in i1 n H5; [cases (not_le_Sn_O ? H);]
           simplify; cases n2; [ repeat rewrite < minus_n_O; apply le_S_S_to_le; assumption]
           cases n1 in H1; [intros; rewrite > eq_minus_n_m_O; apply le_O_n]
@@ -140,18 +147,18 @@ apply (value_of ?? (pred (find ? P f ▭)));
     |2: cases (not_le_Sn_n i1); rewrite > H in ⊢ (??%);
         apply (trans_le ??? ? H4); cases i1 in H3; intros; apply le_S_S; 
         [ apply le_O_n; | assumption]]
-|3: cases (cases_find bar P f ▭); [
+|3: unfold match_domain; cases (cases_find bar (match_pred i) f ▭); [
       cases i1 in H; intros; simplify; [assumption]
       apply lt_S_to_lt; assumption;]
     rewrite > H; cases (\len f) in len_bases_gt_O_f; intros; [cases (not_le_Sn_O ? H3)]
     simplify; apply le_n;
-|4: intros; cases (cases_find bar P f ▭) in H; simplify; intros; 
+|4: intros; unfold match_domain in H; cases (cases_find bar (match_pred i) f ▭) in H; simplify; intros; 
     [1: lapply (H3 n); [2: cases i1 in H4; intros [assumption] apply le_S; assumption;]
-        unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
+        unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
         simplify; intros; [destruct H6] assumption;
     |2: destruct H; cases f in len_bases_gt_O_f H2 H3; clear H1; simplify; intros;
         [cases (not_le_Sn_O ? H)] lapply (H1 n); [2: apply le_S; assumption]
-        unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
+        unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
         simplify; intros; [destruct H4] assumption;]]
 qed.    
 
@@ -167,107 +174,13 @@ intros; cases (value_lemma (bars q) ?? r);
 | apply bars_begin_lt_Qpos;]
 qed.
 
-alias symbol "lt" (instance 5) = "natural 'less than'".
-alias symbol "lt" (instance 4) = "Q less than".
-lemma value_simpl: 
- ∀f:list bar.sorted q2_lt f → O < (length bar f) → 
-  ∀i:ratio.nth_base f O  < Qpos i → ℚ × ℚ.
-intros; cases (value_lemma f H H1 i H2); assumption;
-qed.
-
 lemma cases_value : ∀f,i. value_spec (bars f) (Qpos i) (value f i).
 intros; unfold value; 
 cases (value_lemma (bars f) (bars_sorted f) (len_bases_gt_O f) i (bars_begin_lt_Qpos f i)); 
 assumption;
 qed.
 
-lemma cases_value_simpl :
- ∀f,H1,H2,i,Hi.value_spec f (Qpos i) (value_simpl f H1 H2 i Hi).
-intros; unfold value_simpl; cases (value_lemma f H1 H2 i Hi);
-assumption;
-qed.
-
 definition same_values ≝ λl1,l2:q_f.∀input. value l1 input = value l2 input. 
-definition same_values_simpl ≝ 
-  λl1,l2:list bar.∀H1,H2,H3,H4,input,Hi1,Hi2. 
-   value_simpl l1 H1 H2 input Hi1 = value_simpl l2 H3 H4 input Hi2.
-   
-lemma value_head : 
- ∀x,y,l,H1,H2,i,H3. 
-    Qpos i ≤ \fst x → value_simpl (y::x::l) H1 H2 i H3  = \snd y.
-intros; cases (cases_value_simpl ? H1 H2 i H3);
-cases j in H4 H5 H6 H7 H8 (j); simplify; intros;
-[1: symmetry; assumption;
-|2: cases (?:False); cases j in H4 H5 H6 H7 H8; intros;
-    [1: lapply (q_le_lt_trans ??? H H5) as K;cases (q_lt_corefl ? K);
-    |2: lapply (H7 1); [2: do 2 apply le_S_S; apply le_O_n;]
-        simplify in Hletin; 
-        lapply (q_le_lt_trans ??? H Hletin) as K;cases (q_lt_corefl ? K);]]
-qed.
-
-lemma same_values_simpl_to_same_values: 
-  ∀b1,b2,Hs1,Hs2,Hb1,Hb2,He1,He2,input.
-   same_values_simpl b1 b2 →
-   value (mk_q_f b1 Hs1 Hb1 He1) input =
-   value (mk_q_f b2 Hs2 Hb2 He2) input.
-intros;
-lapply (len_bases_gt_O (mk_q_f b1 Hs1 Hb1 He1));
-lapply (len_bases_gt_O (mk_q_f b2 Hs2 Hb2 He2));
-lapply (H ???? input) as K; try assumption;
-[2: rewrite > Hb1; apply q_pos_OQ;
-|3: rewrite > Hb2; apply q_pos_OQ;
-|1: apply K;]
-qed.
-
-include "russell_support.ma".
-
-lemma value_tail : 
- ∀x,y,l,H1,H2,i,H3. 
-    \fst x < Qpos i → 
-      value_simpl (y::x::l) H1 H2 i H3  = 
-      value_simpl (x::l) ?? i ?.
-[1: apply hide; apply (sorted_tail q2_lt); [apply y| assumption]
-|2: apply hide; simplify; apply le_S_S; apply le_O_n;
-|3: apply hide; assumption;]
-intros;cases (cases_value_simpl ? H1 H2 i H3);
-generalize in ⊢ (? ? ? (? ? % ? ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? % ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? ? ? %)); intro;
-cases (cases_value_simpl (x::l) H9 H10 i H11);
-cut (j = S j1) as E; [ destruct E; destruct H12; reflexivity;]
-clear H12 H4; cases j in H8 H5 H6 H7;
-[1: intros;cases (?:False); lapply (H7 1 (le_n ?)); [2: simplify; do 2 apply le_S_S; apply le_O_n] 
-    simplify in Hletin; apply (q_lt_corefl (\fst x));
-    apply (q_lt_le_trans ??? H Hletin);
-|2: simplify; intros; clear q q1 j H11 H10 H1 H2; simplify in H3 H14; apply eq_f;
-    cases (cmp_nat n j1); [cases (cmp_nat j1 n);[apply le_to_le_to_eq; assumption]]
-    [1: clear H1; cases (?:False);
-        lapply (H7 (S j1)); [2: cases j1 in H2; intros[cases (not_le_Sn_O ? H1)] apply le_S_S; assumption]
-        [2: apply le_S_S; assumption;] simplify in Hletin;
-        apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H13));
-    |2: cases (?:False);
-        lapply (H16 n); [2: assumption|3:simplify; apply le_S_S_to_le; assumption]
-        apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H4));]]
-qed.
-
-lemma value_unit:
-  ∀x,i,h1,h2,h3.value_simpl [x] h1 h2 i h3 = \snd x.
-intros; cases (cases_value_simpl [x] h1 h2 i h3); cases j in H H2; simplify;
-intros; [2: cases (?:False); apply (not_le_Sn_O n); apply le_S_S_to_le; apply H2]
-symmetry; assumption;
-qed.
-
-lemma same_value_tail:
-  ∀b,b1,h1,h3,xs,r1,input,H12,H13,Hi1,H14,H15,Hi2.
-   same_values_simpl (〈b1,h1〉::xs) (〈b1,h3〉::r1) → 
-    value_simpl (b::〈b1,h1〉::xs) H12 H13 input Hi1
-     =value_simpl (b::〈b1,h3〉::r1) H14 H15 input Hi2.
-intros; cases (q_cmp (Qpos input) b1);
-[1: rewrite > (value_head 〈b1,h1〉 b xs); [2:assumption]
-    rewrite > (value_head 〈b1,h3〉 b r1); [2:assumption] reflexivity;
-|2: rewrite > (value_tail 〈b1,h1〉 b xs);[2: assumption]
-    rewrite > (value_tail 〈b1,h3〉 b r1);[2: assumption] apply H;]
-qed.
 
 definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i).
 
@@ -284,5 +197,5 @@ cases (?:False);
 qed.
 
 notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
-interpretation "hide unpos proof" 'unpos x = (unpos x _).
+interpretation "hide unpos proof" 'unpos x = (unpos x ?).