This commit was manufactured by cvs2svn to create branch 'moogle'.

[helm.git] / helm / gTopLevel / esempi / fourier / fourier.cic

diff --git a/helm/gTopLevel/esempi/fourier/fourier.cic b/helm/gTopLevel/esempi/fourier/fourier.cic
deleted file mode 100644 (file)
index 23062f3..0000000
--- a/helm/gTopLevel/esempi/fourier/fourier.cic
+++ /dev/null
@@ -1,137 +0,0 @@
-alias Rge       /Coq/Reals/Rdefinitions/Rge.con
-alias Rle       /Coq/Reals/Rdefinitions/Rle.con
-alias Rgt       /Coq/Reals/Rdefinitions/Rgt.con
-alias Rlt       /Coq/Reals/Rdefinitions/Rlt.con
-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 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
-
-!x:R.
-(Rlt (Rmult(Ropp x)R1)
-R0)
-->(Rlt R0 x)
-
-// test 3x4 -> 35''
-!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 6x6 -> 
-
-!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
-(Rgt
-(Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1)))))))
-  R0)
-->
-(Rgt
-(Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1))))))
-  R0)
-->
-(Rgt
-(Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1)))))
-  R0)
-->
-(Rgt
-(Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1)))))
-  R0)
-->
-(Rgt
-(Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1)))))
-  R0)
-->
-(Rlt
-(Rplus (Rmult (Rplus R1 R1) x) (Rplus v y))
-  R0)
--> (Rlt (Rmult (Rplus R1 R1) x) R0)
-
-
-
-
-
-
-//test base1 ok
-!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
-
-//test base2 ok
-!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
-
-//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 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))
-
-