More work

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 6d936036294637125c97d9253896d9ecc74c5967..f1da6c4979b1a14983719883ecba43a4cda2b720 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -23,9 +23,15 @@ naxiom Qdivides: Q → Q → Q.
 interpretation "Q plus" 'plus x y = (Qplus x y).
 interpretation "Q times" 'times x y = (Qtimes x y).
 interpretation "Q divides" 'divide x y = (Qdivides x y).
-naxiom Qtimes_distr: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
+naxiom Qtimes_plus: ∀n,m:nat.∀q:Q. (n * q + m * q) = (plus n m) * q.
 naxiom Qmult_one: ∀q:Q. 1 * q = q.
 naxiom Qdivides_mult: ∀q1,q2. (q1 * q2) / q1 = q2.
+naxiom Qtimes_distr: ∀q1,q2,q3:Q.(q3 * q1 + q3 * q2) = q3 * (q1 + q2).
+naxiom Qdivides_distr: ∀q1,q2,q3:Q.(q1 / q3 + q2 / q3) = (q1 + q2) / q3.
+naxiom Qplus_comm: ∀q1,q2. q1 + q2 = q2 + q1.
+naxiom Qplus_assoc: ∀q1,q2,q3. q1 + q2 + q3 = q1 + (q2 + q3).
+ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
+#a; #b; #c; //; nqed.
 
 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
 
@@ -46,21 +52,23 @@ ncoinductive locate : Q → Q → Prop ≝
 ndefinition R ≝ ∃l,u:Q. locate l u.
 
 nlet corec Q_to_locate q : locate q q ≝ L q q ?.
- ncut (locate q q = locate q ((2*q+q)/3))
+ ncut (q = (2*q+q)/3)
   [##2: #H; ncases H; (*NOT WORKING: nrewrite > H;*) napply Q_to_locate
-  | //;
-  ##]
+  |nrewrite < (Qdivides_mult 3 q) in ⊢ (? ? % ?);//
+  ]
 nqed.
 
 ndefinition Q_to_R : Q → R.
  #q; @ q; @q; //.
 nqed.
 
-(*
 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
  locate (l1 + l2) (u1 + u2) ≝ ?.
  ncases r1; ncases r2; #l2; #u2; #r2; #l1; #u1; #r1
-  [ @1; napply locate_add;
+  [ ##1: @1; napplyS (locate_add … r1 …r2);
+  ##|##4: @2; napplyS (locate_add … r1 …r2);
+  ##| ncases r2; #l2'; #u2'; #r2';
+    .
  
 nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0] ≝
  match disjoint l1 u1 l2 u2 with