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

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index 09caea79b..ba51e64ad 100644
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -6,10 +6,43 @@ alias Ropp     /Coq/Reals/Rdefinitions/Ropp.con
 alias Rinv     /Coq/Reals/Rdefinitions/Rinv.con
 alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
 alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
+alias Rmult    /Coq/Reals/Rdefinitions/Rmult.con
 alias R1        /Coq/Reals/Rdefinitions/R1.con
 alias R0        /Coq/Reals/Rdefinitions/R0.con
 alias R        /Coq/Reals/Rdefinitions/R.con
-alias Eq	/Coq/Init/Logic_Type/eqT.ind#1/1
+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))
@@ -17,17 +50,48 @@ alias Eq	/Coq/Init/Logic_Type/eqT.ind#1/1
 //test base2 ok
 !x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
 
-//test base3 (unification fails)
+//test base3 ok
 !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
 
+/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
+
+intros
+
+/Coq/Init/Logic/False.ind#1/1
+
+(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))
 
 //test base5 ok
 !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
 
-//test base6 (unification fails)
-!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
+//test base6 ok
+!x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
 
 //test base7 (should fail) ok
 !x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))