helm/gTopLevel/esempi/fourier.cic

   1 alias Rge       /Coq/Reals/Rdefinitions/Rge.con
   2 alias Rle       /Coq/Reals/Rdefinitions/Rle.con
   3 alias Rgt       /Coq/Reals/Rdefinitions/Rgt.con
   4 alias Rlt       /Coq/Reals/Rdefinitions/Rlt.con
   5 alias Ropp     /Coq/Reals/Rdefinitions/Ropp.con
   6 alias Rinv     /Coq/Reals/Rdefinitions/Rinv.con
   7 alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
   8 alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
   9 alias Rmult    /Coq/Reals/Rdefinitions/Rmult.con
  10 alias R1        /Coq/Reals/Rdefinitions/R1.con
  11 alias R0        /Coq/Reals/Rdefinitions/R0.con
  12 alias R        /Coq/Reals/Rdefinitions/R.con
  13 alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
  14 alias not      /Coq/Init/Logic/not.con
  15 alias or /Coq/Init/Logic/or.ind#1/1
  16
  17 (*test real*)
  18 !x:R.!y:R.!z:R.
  19 (Rge
  20 (Rplus
  21  (Rmult (Ropp (Rplus R1 R1)) x) (Rplus
  22    (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus
  23      (Rmult (Rplus R1 (Rplus R1 R1)) z) R1)
  24 )) R0)
  25 ->
  26 (Rge
  27 (Rplus
  28  (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus
  29    (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus
  30       R1 (Rplus R1 R1))
  31 )) R0)
  32 ->
  33 (Rgt
  34 (Rplus
  35   x (Rplus
  36    (Rmult (Rplus R1 R1) y) (Ropp z) )
  37 ) R0)
  38 ->
  39 (Rgt
  40 (Rplus
  41  (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus
  42    z (Ropp R1))
  43 ) R0)
  44
  45 -> (Rlt z R1)
  46
  47 //test base1 ok
  48 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
  49
  50 //test base2 ok
  51 !x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
  52
  53 //test base3 ok
  54 !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
  55
  56 /Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
  57
  58 intros
  59
  60 /Coq/Init/Logic/False.ind#1/1
  61
  62 (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))))
  63
  64 /Coq/fourier/Fourier_util/Rnot_le_le.con
  65
  66 t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
  67
  68 t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
  69
  70 (t1-t2)=(Rminus
  71 (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
  72 (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))
  73
  74 tc=(Rmult (Ropp R1) (Rinv R1))
  75
  76 rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
  77  (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1)))
  78
  79 change=(not (or
  80 (Rlt R0 (Rmult (Ropp R1) (Rinv R1)))
  81 (eqT R R0 (Rmult (Ropp R1) (Rinv R1)))
  82 ))
  83
  84 tac2
  85 /Coq/fourier/Fourier_util/Rnot_lt0.con
  86
  87 //test base4 ok
  88 !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
  89
  90 //test base5 ok
  91 !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
  92
  93 //test base6 ok
  94 !x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
  95
  96 //test base7 (should fail) ok
  97 !x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))
  98
  99