more work to try to understand where the issue is

[helm.git] / helm / software / matita / contribs / dama / dama / models / q_bars.ma

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 249abdf6c2b47d1e98f32f7ab497097c0e564c5a..d0d043f47e053ae50df4e8aaba1ac9f510a83d72 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -29,7 +29,7 @@ interpretation "q0" 'empty_bar = empty_bar.
 notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}.
 interpretation "lq2" 'lq2 = (list bar).
 
-let rec sum_bases (l:list bar) (i:nat)on i ≝
+let rec sum_bases (l:list bar) (i:nat) on i ≝
     match i with
     [ O ⇒ OQ
     | S m ⇒ 
@@ -128,8 +128,8 @@ definition hide ≝ λT:Type.λx:T.x.
 interpretation "hide" 'hide = (hide _ _).
 
 lemma sum_bases_ge_OQ:
-  ∀l,n. OQ ≤ sum_bases (bars l) n.
-intro; elim (bars l); simplify; intros;
+  ∀l,n. OQ ≤ sum_bases l n.
+intro; elim l; simplify; intros;
 [1: elim n; [apply q_eq_to_le;reflexivity] simplify;
     apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ;
 |2: cases n; [apply q_eq_to_le;reflexivity] simplify; 
@@ -144,7 +144,43 @@ cases (q_le_cases ?? H);
 |2: apply (q_lt_antisym ??? H1);] clear H H1; cases (bars l);
 simplify; apply q_lt_plus_trans;
 try apply q_pos_lt_OQ; 
-try apply (sum_bases_ge_OQ (mk_q_f OQ []));
-apply (sum_bases_ge_OQ (mk_q_f OQ l1));
+try apply (sum_bases_ge_OQ []);
+apply (sum_bases_ge_OQ l1);
+qed.
+
+lemma sum_bases_increasing:
+  ∀l,x.sum_bases l x < sum_bases l (S x). 
+intro; elim l;
+[1: elim x;
+    [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+        apply q_pos_lt_OQ;
+    |2: simplify in H ⊢ %; 
+        apply q_lt_plus; rewrite > q_elim_minus;
+        rewrite < q_plus_assoc; rewrite < q_elim_minus;
+        rewrite > q_plus_minus; rewrite > q_plus_OQ;
+        assumption;]
+|2: elim x;
+    [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ;
+        apply q_pos_lt_OQ;
+    |2: simplify; change in ⊢ (? ? (? % ?)) with (sum_bases l1 (S n)) ;  
+        apply q_lt_plus; rewrite > q_elim_minus;
+        rewrite < q_plus_assoc; rewrite < q_elim_minus;
+        rewrite > q_plus_minus; rewrite > q_plus_OQ; apply H]]
+qed.
+
+lemma sum_bases_lt_canc:
+  ∀l,x,y.sum_bases l (S x) < sum_bases l (S y) → sum_bases l x < sum_bases l y.
+intro; elim l; [apply (q_lt_canc_plus_r ?? (Qpos one));apply H]
+generalize in match H1;apply (nat_elim2 (?:? → ? → CProp) ??? x y);
+intros 2;
+[3: intros 2; simplify; apply q_lt_inj_plus_r; apply H;
+    apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H3;
+|2: cases (?:False); simplify in H2;
+    apply (q_lt_le_incompat (sum_bases l1 (S n)) OQ);[2: apply sum_bases_ge_OQ;]
+    apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H2;
+|1: cases n in H2; intro; 
+    [1: cases (?:False); apply (q_lt_corefl ? H2);
+    |2: simplify; apply  q_lt_plus_trans; [apply sum_bases_ge_OQ]
+        apply q_pos_lt_OQ;]]
 qed.