Not is now inductive.

[helm.git] / helm / software / matita / nlibrary / arithmetics / R.ma

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 9087304bdda0c7b30d99627deb990f9d3991abc3..e113fabf3c5b3572fc9e33229a14f58a8cc770e5 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -51,18 +51,13 @@ 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.
 
-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.
- λHterm:locate x1 x2.
-  (λHcut:x1=x1 → x2=x2 → P x1 x2. Hcut (refl Q x1) (refl Q x2))
-   match Hterm return λy1,y2.λp:locate y1 y2.
-    x1=y1 → x2=y2 →P x1 x2
-   with
-    [ L l l' u' u Hle1 Hle2 r ⇒ ?(*H1 l l' u' u ?*)
-    | H l l' u' u Hle1 Hle2 r ⇒ ?(*H2 l l' u' u ?*)].
-#a; #b; ##[ napply (H2 … r …) ##| napply (H1 … r …) ##] //.
+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.
 nqed.
 
 ndefinition R ≝ ∃l,u:Q. locate l u.
@@ -78,7 +73,7 @@ nqed.
 (*
 nlet corec locate_add (l1,u1:?) (r1: locate l1 u1) (l2,u2:?) (r2: locate l2 u2) :
  locate (l1 + l2) (u1 + u2) ≝ ?.
- ninversion r1; ninversion r2; #l2'; #u2'; #leq2l; #leq2u; #r2;
+ napply (locate_inv_ind' … r1); napply (locate_inv_ind' … r2); #l2'; #u2'; #leq2l; #leq2u; #r2;
  #l1'; #u1'; #leq1l; #leq1u; #r1
   [ ##1,4: ##[ @1 ? (l1'+l2') (u1'+u2') | @2 ? (l1'+l2') (u1'+u2') ]
     ##[ ##1,5: /2/ | napplyS (Qle_plus_compat …leq1u leq2u) |
@@ -169,16 +164,14 @@ nqed.
 ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝
 | ftfish : ∀a.
     a ∈ F →
-    (*(∀i:𝐈 a .∃b. b ∈ 𝐂  a i ∧ ftfish A F b) →*)
     (∀b. a ≤ b → ftfish A F b) →
-    (∀b. a ≤ b → ∀i:𝐈 b. ∃x.  x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftcover A F x) →
+    (∀b. a ≤ b → ∀i:𝐈 b. ∃x.  x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftfish A F x) →
     ftfish A F a.
 
-ntheorem 
-
-interpretation "fish" 'fish a U = (fish ? U a).
+interpretation "fish" 'fish a U = (ftfish ? U a).
 
 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; *; #b; #H; #H1; #i; @ a; @; //;
- ncases H;  
\ No newline at end of file
+ #A; #F; #a; #H; ncases H; #b; #_; #_; #H2; #i; ncases (H2 … i); //;
+ #x; *; *; *; #y; *; #K2; #K3; #_; #K5; @y; @ K2; ncases K5 in K3; /2/.
+nqed.
\ No newline at end of file