From 6b61a9e6698a7c1936adf217b599e34e65a5e4c9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 26 Jun 2008 21:35:10 +0000
Subject: [PATCH] more work

---
 .../contribs/dama/dama/models/q_bars.ma       |  8 +++----
 .../contribs/dama/dama/models/q_function.ma   | 21 ++++++++++++++-----
 .../contribs/dama/dama/models/q_support.ma    |  5 ++++-
 3 files changed, 24 insertions(+), 10 deletions(-)

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 249abdf6c..6be729db5 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -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,7 @@ 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.
 
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 bb3ba55fc..321223710 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -64,16 +64,27 @@ whd in ⊢ (% → ?); simplify in H3;
         |2: cases n in H5 H6; [intros; reflexivity] intros;
             cases (?:False); clear H6; cases (bars l1) in H5; simplify; intros;
             [apply (q_pos_OQ one);|apply (q_pos_OQ (\fst b));] 
-            apply (q_le_S ??? (sum_bases_ge_OQ (mk_q_f init ?) n1));[apply [];|3:apply l]
-            simplify in ⊢ (? (? (? % ?) ?) ?); rewrite < (q_plus_minus w);
-            apply q_le_minus_r; rewrite < q_minus_r; 
-            rewrite < E in ⊢ (??%); assumption;]
+            apply (q_le_S ??? (sum_bases_ge_OQ ? n1));[apply []|3:apply l]
+            simplify in ⊢ (? (? (? % ?) ?) ?); rewrite < (q_plus_minus (Qpos w));
+            rewrite > q_elim_minus; apply q_le_minus_r; 
+            rewrite > q_elim_opp; rewrite < E in ⊢ (??%); assumption;]
     |2: intros; rewrite > H8; rewrite > H7; clear H8 H7;
         simplify in H5 H6 ⊢ %; 
         cases (\fst w1) in H5 H6; [intros; reflexivity]
         cases (bars l1);
         [1: intros; simplify; elim n [reflexivity] simplify; assumption;
-        |2: simplify; intros; cases (?:False);
+        |2: simplify; intros; cases (?:False); clear H6;
+            apply (q_lt_le_incompat (input - init) (Qpos w) );
+            [1: rewrite > H2; do 2 rewrite > q_elim_minus;
+                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: rewrite < q_d_noabs; [2: apply q_lt_to_le; assumption]
+                rewrite > q_d_sym; apply (q_le_S ???? H5);
+                apply sum_bases_ge_OQ;]]
+    |3:
+    
         
 STOP            
         
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 4b80d92cf..f10113d50 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -27,10 +27,12 @@ interpretation "Q minus" 'minus x y = (qm x y).
 
 axiom q_plus_OQ: ∀x:ℚ.x + OQ = x.
 axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x.
-axiom q_plus_minus: ∀x.Qpos x + Qneg x = OQ.
+axiom q_plus_minus: ∀x.x - x = OQ.
 axiom q_minus: ∀x,y. y - Qpos x = y + Qneg x.
 axiom q_minus_r: ∀x,y. y + Qpos x = y - Qneg x.
 axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z. 
+axiom q_elim_minus: ∀x,y.x - y = x + Qopp y.
+axiom q_elim_opp: ∀x,y.x - Qopp y = x + y.
 
 (* order over Q *)
 axiom qlt : ℚ → ℚ → CProp.
@@ -54,6 +56,7 @@ axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
 axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a.
 axiom q_lt_corefl: ∀x:Q.x < x → False.
 axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
+axiom q_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False.
 axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
 axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
 axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
-- 
2.39.2