X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Ffourier.cic;h=ba51e64ad80b3a8ee7dab716b0b34e6b93fe4f3f;hb=7e9ee837f75f38bf01240cdc03dd51c764c2665f;hp=dc883e4e4888fd11463339122b528af7320bd3d7;hpb=d64cc26e9b740fb375f46f6d9e39d42802db3ff7;p=helm.git

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index dc883e4e4..ba51e64ad 100644
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -12,7 +12,37 @@ alias R0        /Coq/Reals/Rdefinitions/R0.con
 alias R        /Coq/Reals/Rdefinitions/R.con
 alias eqT	/Coq/Init/Logic_Type/eqT.ind#1/1
 alias not      /Coq/Init/Logic/not.con
-
+alias or /Coq/Init/Logic/or.ind#1/1
+
+(*test real*)
+!x:R.!y:R.!z:R.
+(Rge
+(Rplus
+ (Rmult (Ropp (Rplus R1 R1)) x) (Rplus 
+   (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus 
+     (Rmult (Rplus R1 (Rplus R1 R1)) z) R1)
+)) R0)
+->  
+(Rge
+(Rplus
+ (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus 
+   (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus 
+      R1 (Rplus R1 R1))
+)) R0)
+->  
+(Rgt
+(Rplus
+  x (Rplus 
+   (Rmult (Rplus R1 R1) y) (Ropp z) )
+) R0)
+-> 
+(Rgt
+(Rplus
+ (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus 
+   z (Ropp R1))
+) R0)
+
+-> (Rlt z R1)
 
 //test base1 ok
 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
@@ -25,19 +55,35 @@ alias not      /Coq/Init/Logic/not.con
 
 /Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
 
+intros
+
 /Coq/Init/Logic/False.ind#1/1
 
-(Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))
+(not (Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))))
 
 /Coq/fourier/Fourier_util/Rnot_le_le.con
 
 t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
+
 t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
+
+(t1-t2)=(Rminus 
+(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
+(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))
+
 tc=(Rmult (Ropp R1) (Rinv R1))
 
 rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
  (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1)))
 
+change=(not (or 
+(Rlt R0 (Rmult (Ropp R1) (Rinv R1))) 
+(eqT R R0 (Rmult (Ropp R1) (Rinv R1))) 
+))
+
+tac2
+/Coq/fourier/Fourier_util/Rnot_lt0.con
+
 //test base4 ok
 !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))