From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Apr 2010 13:28:53 +0000 (+0000)
Subject: Some dualization clean-up.
X-Git-Tag: make_still_working~2924
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=395bcb2796cb9edcdb792579341c2271a8d1adaf;p=helm.git

Some dualization clean-up.

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

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index e113fabf3..d58f69a05 100644
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -17,12 +17,16 @@ include "arithmetics/nat.ma".
 naxiom Q: Type[0].
 naxiom nat_to_Q: nat → Q.
 ncoercion nat_to_Q : ∀x:nat.Q ≝ nat_to_Q on _x:nat to Q.
+ndefinition bool_to_nat ≝ λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
+ncoercion bool_to_nat : ∀b:bool.nat ≝ bool_to_nat on _b:bool to nat.
 naxiom Qplus: Q → Q → Q.
+naxiom Qminus: Q → Q → Q.
 naxiom Qtimes: Q → Q → Q.
 naxiom Qdivides: Q → Q → Q.
 naxiom Qle : Q → Q → Prop.
 naxiom Qlt: Q → Q → Prop.
 interpretation "Q plus" 'plus x y = (Qplus x y).
+interpretation "Q minus" 'minus x y = (Qminus x y).
 interpretation "Q times" 'times x y = (Qtimes x y).
 interpretation "Q divides" 'divide x y = (Qdivides x y).
 interpretation "Q le" 'leq x y = (Qle x y).
@@ -39,7 +43,10 @@ ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
 naxiom Qle_refl: ∀q1. q1≤q1.
 naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
 naxiom Qle_plus_compat: ∀x,y,z,t. x≤y → z≤t → x+z ≤ y+t.
+naxiom Qmult_zero: ∀q:Q. 0 * q = 0.
 
+naxiom phi: Q. (* the golden number *)
+naxiom golden: phi = phi * phi + phi * phi * phi.
 
 (* naxiom Ndivides_mult: ∀n:nat.∀q. (n * q) / n = q. *)
 
@@ -47,28 +54,60 @@ ntheorem lem1: ∀n:nat.∀q:Q. (n * q + q) = (S n) * q.
 #n; #q; ncut (plus n 1 = S n);##[//##]
 //; nqed.
 
+ntheorem Qplus_zero: ∀q:Q. 0 + q = q. //. nqed.
+
 ncoinductive locate : Q → Q → Prop ≝
-   L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u
- | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u.
+   L: ∀l,u. locate l ((1 - phi) * l + phi * u) → locate l u
+ | H: ∀l,u. locate (phi * l + (1 - phi) * u) u → locate l u.
 
 ndefinition locate_inv_ind':
- ∀x1,x2:Q.∀P:Q → Q → Prop.
-  ∀H1: ∀l',u'.x1≤l' → u'≤((2 * x1 + x2) / 3) → locate l' u' → P x1 x2. 
-  ∀H2: ∀l',u'. ((x1 + 2 * x2) / 3)≤l' → u'≤ x2 → locate l' u' → P x1 x2.
-   locate x1 x2 → P x1 x2.
- #x1; #x2; #P; #H1; #H2; #p; ninversion p; #l; #l'; #u'; #u; #Ha; #Hb; #E1;
- #E2; #E3; ndestruct; /2/ width=5.
+ ∀l,u:Q.∀P:Q → Q → Prop.
+  ∀H1: locate l ((1 - phi) * l + phi * u) → P l u. 
+  ∀H2: locate (phi * l + (1 - phi) * u) u → P l u.
+   locate l u → P l u.
+ #l; #u; #P; #H1; #H2; #p; ninversion p; #l; #u; #H; #E1; #E2;
+ ndestruct; /2/.
 nqed.
 
 ndefinition R ≝ ∃l,u:Q. locate l u.
 
-nlet corec Q_to_locate q : locate q q ≝ L q q q q … (Q_to_locate q).
+(*
+nlet corec Q_to_locate q : locate q q ≝ L q q … (Q_to_locate q).
   //; nrewrite < (Qdivides_mult 3 q) in ⊢ (? % ?); //.
 nqed.
 
 ndefinition Q_to_R : Q → R.
  #q; @ q; @q; //.
 nqed.
+*)
+
+nlemma help_auto1: ∀q:Q. false * q = 0. #q; nnormalize; //. nqed.
+
+(*
+nlet corec locate_add (l,u:?) (r1,r2: locate l u) (c1,c2:bool) :
+ locate (l + l + c1 * phi + c2 * phi * phi) (u + u + c1 * phi + c2 * phi * phi) ≝ ?.
+ napply (locate_inv_ind' … r1); napply (locate_inv_ind' … r2);
+ #r2'; #r1'; ncases c1; ncases c2
+  [ ##4: nnormalize; @1;
+    nlapply (locate_add … r1' r2' false false); nnormalize;
+    nrewrite > (Qmult_zero …); nrewrite > (Qmult_zero …); #K; nauto demod;
+     #K;
+    nnormalize in K; nrewrite > (Qmult_zero …) in K; nnormalize; #K;
+    napplyS K;
+     
+
+
+ 
+  [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
+    ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
+        ##4: napplyS (Qle_plus_compat …leq1l leq2l)
+      |##*: /2/ ]
+ ##| ninversion r2; #l2''; #u2''; #leq2l'; #leq2u'; #r2';
+     ninversion r1; #l1''; #u1''; #leq1l'; #leq1u'; #r1';
+      ##[ @1 ? (l1''+l2'') (u1''+u2''); 
+      ##[ napply Qle_plus_compat; /3/;
+        ##| ##3: /2/;
+        ##| napplyS (Qle_plus_compat …leq1u' leq2u');
 
 (*
 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
@@ -92,6 +131,7 @@ nlet corec apart (l1,u1) (r1: locate l1 u1) (l2,u2) (r2: locate l2 u2) : CProp[0
   [ true ⇒ True
   | false ⇒ 
 *)
+*)
 
 include "topology/igft.ma".
 include "datatypes/pairs.ma".
@@ -157,7 +197,7 @@ interpretation "ftcovers" 'covers a U = (ftcover ? U a).
 ntheorem ftinfinity: ∀A: Ax_pro. ∀U: Ω^A. ∀a. ∀i. (∀x. x ∈ 𝐂 a i → x ◃ U) → a ◃ U.
  #A; #U; #a; #i; #H;
  napply (ftleqinfinity … a … i); //;
- #x; *; *; #b; *; #H1; #H2; #H3; napply (ftleqleft … b); //;
+ #b; *; *; #b; *; #H1; #H2; #H3; napply (ftleqleft … b); //;
  napply H; napply H1 (*CSC: auto non va! *).
 nqed.
 
@@ -170,8 +210,25 @@ ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝
 
 interpretation "fish" 'fish a U = (ftfish ? U a).
 
+nlemma ftcoreflexivity: ∀A: Ax_pro.∀F.∀a:A. a ⋉ F → a ∈ F.
+ #A; #F; #a; #H; ncases H; //.
+nqed.
+
+nlemma ftcoleqinfinity:
+ ∀A: Ax_pro.∀F.∀a:A. a ⋉ F →
+  ∀b. (a ≤ b → ∀i. (∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ x ⋉ F)).
+ #A; #F; #a; #H; ncases H; /2/.
+nqed.
+
+nlemma ftcoleqleft:
+ ∀A: Ax_pro.∀F.∀a:A. a ⋉ F →
+  (∀b. a ≤ b → b ⋉ F).
+ #A; #F; #a; #H; ncases H; /2/.
+nqed.
+
 alias symbol "I" (instance 6) = "I".
 ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
- #A; #F; #a; #H; ncases H; #b; #_; #_; #H2; #i; ncases (H2 … i); //;
- #x; *; *; *; #y; *; #K2; #K3; #_; #K5; @y; @ K2; ncases K5 in K3; /2/.
+ #A; #F; #a; #H; #i; nlapply (ftcoleqinfinity … F … a … i); //; #H;
+ ncases H; #c; *; *; *; #b; *; #H1; #H2; #H3; #H4; @ b; @ [ napply H1 (*CSC: auto non va *)]
+ napply (ftcoleqleft … c); //.
 nqed.
\ No newline at end of file